:: UNIALG_2 semantic presentation

NAT is non empty V29() V30() V31() V36() V41() V42() Element of bool REAL
REAL is set
bool REAL is non empty set
NAT is non empty V29() V30() V31() V36() V41() V42() set
bool NAT is non empty V36() set
bool NAT is non empty V36() set
K229() is non empty set
0 is empty functional V29() V30() V31() V33() V34() V35() V36() V41() V43( {} ) FinSequence-membered V89() Element of NAT
{} is empty functional V29() V30() V31() V33() V34() V35() V36() V41() V43( {} ) FinSequence-membered V89() set
the empty functional V29() V30() V31() V33() V34() V35() V36() V41() V43( {} ) FinSequence-membered V89() set is empty functional V29() V30() V31() V33() V34() V35() V36() V41() V43( {} ) FinSequence-membered V89() set
1 is non empty set
{0,1} is non empty set
2 is non empty set
3 is non empty set
Seg 1 is Element of bool NAT
{1} is non empty trivial V43(1) set
Seg 2 is Element of bool NAT
{1,2} is non empty set
dom {} is set
rng {} is set
a is non empty V84() quasi_total non-empty UAStr

b is non empty V84() quasi_total non-empty UAStr

a is non empty V84() quasi_total non-empty UAStr

U0 is non empty V84() quasi_total non-empty UAStr
the charact of U0 is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of U0 *), the carrier of U0) -valued Function-like Function-yielding V36() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of U0 *), the carrier of U0)
the carrier of U0 is non empty set
the carrier of U0 * is non empty functional FinSequence-membered FinSequenceSet of the carrier of U0
PFuncs (( the carrier of U0 *), the carrier of U0) is non empty functional set
len the charact of U0 is non empty V29() V30() V31() V35() V36() V41() Element of NAT
L is non empty V84() quasi_total non-empty UAStr
the charact of L is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of L *), the carrier of L) -valued Function-like Function-yielding V36() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of L *), the carrier of L)
the carrier of L is non empty set
the carrier of L * is non empty functional FinSequence-membered FinSequenceSet of the carrier of L
PFuncs (( the carrier of L *), the carrier of L) is non empty functional set
len the charact of L is non empty V29() V30() V31() V35() V36() V41() Element of NAT

len () is V29() V30() V31() V35() V36() V41() Element of NAT

len () is V29() V30() V31() V35() V36() V41() Element of NAT
U0 is non empty V84() quasi_total non-empty UAStr
L is non empty V84() quasi_total non-empty UAStr
a is non empty V84() quasi_total non-empty UAStr

U0 is non empty V84() quasi_total non-empty UAStr
the charact of U0 is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of U0 *), the carrier of U0) -valued Function-like Function-yielding V36() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of U0 *), the carrier of U0)
the carrier of U0 is non empty set
the carrier of U0 * is non empty functional FinSequence-membered FinSequenceSet of the carrier of U0
PFuncs (( the carrier of U0 *), the carrier of U0) is non empty functional set
rng the charact of U0 is set
bool (PFuncs (( the carrier of U0 *), the carrier of U0)) is non empty set
U0 is non empty V84() quasi_total non-empty UAStr
the charact of U0 is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of U0 *), the carrier of U0) -valued Function-like Function-yielding V36() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of U0 *), the carrier of U0)
the carrier of U0 is non empty set
the carrier of U0 * is non empty functional FinSequence-membered FinSequenceSet of the carrier of U0
PFuncs (( the carrier of U0 *), the carrier of U0) is non empty functional set
rng the charact of U0 is set
L is non empty set
dom the charact of U0 is Element of bool NAT
a is Element of L
b is V29() V30() V31() V35() V36() V41() set
the charact of U0 . b is homogeneous set
[:( the carrier of U0 *), the carrier of U0:] is non empty set
bool [:( the carrier of U0 *), the carrier of U0:] is non empty set
x is Relation-like the carrier of U0 * -defined the carrier of U0 -valued Function-like Element of bool [:( the carrier of U0 *), the carrier of U0:]
U0 is non empty V84() quasi_total non-empty UAStr
the carrier of U0 is non empty set
bool the carrier of U0 is non empty set
the carrier of U0 * is non empty functional FinSequence-membered FinSequenceSet of the carrier of U0
(U0) is non empty PFuncsDomHQN of the carrier of U0
the charact of U0 is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of U0 *), the carrier of U0) -valued Function-like Function-yielding V36() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of U0 *), the carrier of U0)
PFuncs (( the carrier of U0 *), the carrier of U0) is non empty functional set
rng the charact of U0 is set
U0 is non empty V84() quasi_total non-empty UAStr
the carrier of U0 is non empty set
bool the carrier of U0 is non empty set
U0 is non empty V84() quasi_total non-empty UAStr
the carrier of U0 is non empty set
bool the carrier of U0 is non empty set
the carrier of U0 * is non empty functional FinSequence-membered FinSequenceSet of the carrier of U0
(U0) is non empty PFuncsDomHQN of the carrier of U0
the charact of U0 is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of U0 *), the carrier of U0) -valued Function-like Function-yielding V36() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of U0 *), the carrier of U0)
PFuncs (( the carrier of U0 *), the carrier of U0) is non empty functional set
rng the charact of U0 is set
L is non empty Element of bool the carrier of U0
a is non empty Relation-like the carrier of U0 * -defined the carrier of U0 -valued Function-like homogeneous quasi_total Element of (U0)
arity a is V29() V30() V31() V35() V36() V41() Element of NAT
() -tuples_on L is non empty functional FinSequence-membered FinSequenceSet of L
a | (() -tuples_on L) is Relation-like the carrier of U0 * -defined the carrier of U0 -valued Function-like Element of bool [:( the carrier of U0 *), the carrier of U0:]
[:( the carrier of U0 *), the carrier of U0:] is non empty set
bool [:( the carrier of U0 *), the carrier of U0:] is non empty set

[:(L *),L:] is non empty set
bool [:(L *),L:] is non empty set
() -tuples_on the carrier of U0 is non empty functional FinSequence-membered FinSequenceSet of the carrier of U0
b is set
{ } is set

len x is V29() V30() V31() V35() V36() V41() Element of NAT
rng x is set

{ b1 where b1 is Relation-like NAT -defined the carrier of U0 -valued Function-like V36() FinSequence-like FinSubsequence-like Element of the carrier of U0 * : len b1 = arity a } is set
dom (a | (() -tuples_on L)) is functional FinSequence-membered set

(dom a) /\ (() -tuples_on L) is set
(() -tuples_on the carrier of U0) /\ (() -tuples_on L) is set
rng (a | (() -tuples_on L)) is set
b is set
x is set
(a | (() -tuples_on L)) . x is set
{ } is set

len y is V29() V30() V31() V35() V36() V41() Element of NAT
(a | (() -tuples_on L)) . y is set
a . y is set
{ (b1 -tuples_on L) where b1 is V29() V30() V31() V35() V36() V41() Element of NAT : verum } is set
union { (b1 -tuples_on L) where b1 is V29() V30() V31() V35() V36() V41() Element of NAT : verum } is set

len x is V29() V30() V31() V35() V36() V41() Element of NAT
len y is V29() V30() V31() V35() V36() V41() Element of NAT
{ } is set

len y is V29() V30() V31() V35() V36() V41() Element of NAT

len z is V29() V30() V31() V35() V36() V41() Element of NAT

len x is V29() V30() V31() V35() V36() V41() Element of NAT

len y is V29() V30() V31() V35() V36() V41() Element of NAT
{ } is set

len y is V29() V30() V31() V35() V36() V41() Element of NAT
U0 is non empty V84() quasi_total non-empty UAStr
the carrier of U0 is non empty set
bool the carrier of U0 is non empty set
L is non empty Element of bool the carrier of U0

PFuncs ((L *),L) is non empty functional set
the charact of U0 is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of U0 *), the carrier of U0) -valued Function-like Function-yielding V36() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of U0 *), the carrier of U0)
the carrier of U0 * is non empty functional FinSequence-membered FinSequenceSet of the carrier of U0
PFuncs (( the carrier of U0 *), the carrier of U0) is non empty functional set
dom the charact of U0 is Element of bool NAT
(U0) is non empty PFuncsDomHQN of the carrier of U0
rng the charact of U0 is set
len the charact of U0 is non empty V29() V30() V31() V35() V36() V41() Element of NAT
Seg (len the charact of U0) is non empty V36() V43( len the charact of U0) Element of bool NAT
a is V29() V30() V31() V35() V36() V41() set
the charact of U0 . a is homogeneous set
b is non empty Relation-like the carrier of U0 * -defined the carrier of U0 -valued Function-like homogeneous quasi_total Element of (U0)
(U0,L,b) is non empty Relation-like L * -defined L -valued Function-like homogeneous quasi_total Element of bool [:(L *),L:]
[:(L *),L:] is non empty set
bool [:(L *),L:] is non empty set
x is Element of PFuncs ((L *),L)
y is non empty Relation-like the carrier of U0 * -defined the carrier of U0 -valued Function-like homogeneous quasi_total Element of (U0)
(U0,L,y) is non empty Relation-like L * -defined L -valued Function-like homogeneous quasi_total Element of bool [:(L *),L:]

dom a is Element of bool NAT

dom b is Element of bool NAT
x is set
the charact of U0 . x is homogeneous set
b . x is set
y is non empty Relation-like the carrier of U0 * -defined the carrier of U0 -valued Function-like homogeneous quasi_total Element of (U0)
(U0,L,y) is non empty Relation-like L * -defined L -valued Function-like homogeneous quasi_total Element of bool [:(L *),L:]
[:(L *),L:] is non empty set
bool [:(L *),L:] is non empty set

dom a is Element of bool NAT

dom b is Element of bool NAT
x is V29() V30() V31() V35() V36() V41() set
a . x is set
b . x is set
the charact of U0 . x is homogeneous set
y is non empty Relation-like the carrier of U0 * -defined the carrier of U0 -valued Function-like homogeneous quasi_total Element of (U0)
(U0,L,y) is non empty Relation-like L * -defined L -valued Function-like homogeneous quasi_total Element of bool [:(L *),L:]
[:(L *),L:] is non empty set
bool [:(L *),L:] is non empty set
U0 is non empty V84() quasi_total non-empty UAStr
the carrier of U0 is non empty set
bool the carrier of U0 is non empty set
the carrier of U0 * is non empty functional FinSequence-membered FinSequenceSet of the carrier of U0
(U0) is non empty PFuncsDomHQN of the carrier of U0
the charact of U0 is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of U0 *), the carrier of U0) -valued Function-like Function-yielding V36() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of U0 *), the carrier of U0)
PFuncs (( the carrier of U0 *), the carrier of U0) is non empty functional set
rng the charact of U0 is set
L is non empty Element of bool the carrier of U0
a is non empty Relation-like the carrier of U0 * -defined the carrier of U0 -valued Function-like homogeneous quasi_total Element of (U0)

len b is V29() V30() V31() V35() V36() V41() Element of NAT
arity a is V29() V30() V31() V35() V36() V41() Element of NAT
a . b is set

() -tuples_on L is non empty functional FinSequence-membered FinSequenceSet of L
(len b) -tuples_on L is non empty functional FinSequence-membered FinSequenceSet of L
rng a is set
a is non empty Relation-like the carrier of U0 * -defined the carrier of U0 -valued Function-like homogeneous quasi_total Element of (U0)
(U0,L,a) is non empty Relation-like L * -defined L -valued Function-like homogeneous quasi_total Element of bool [:(L *),L:]

[:(L *),L:] is non empty set
bool [:(L *),L:] is non empty set

arity a is V29() V30() V31() V35() V36() V41() Element of NAT
() -tuples_on L is non empty functional FinSequence-membered FinSequenceSet of L
a | (() -tuples_on L) is Relation-like the carrier of U0 * -defined the carrier of U0 -valued Function-like Element of bool [:( the carrier of U0 *), the carrier of U0:]
[:( the carrier of U0 *), the carrier of U0:] is non empty set
bool [:( the carrier of U0 *), the carrier of U0:] is non empty set
a is non empty Relation-like the carrier of U0 * -defined the carrier of U0 -valued Function-like homogeneous quasi_total Element of (U0)
(U0,L,a) is non empty Relation-like L * -defined L -valued Function-like homogeneous quasi_total Element of bool [:(L *),L:]

[:(L *),L:] is non empty set
bool [:(L *),L:] is non empty set
U0 is non empty V84() quasi_total non-empty UAStr
the carrier of U0 is non empty set
bool the carrier of U0 is non empty set
the carrier of U0 * is non empty functional FinSequence-membered FinSequenceSet of the carrier of U0
(U0) is non empty PFuncsDomHQN of the carrier of U0
the charact of U0 is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of U0 *), the carrier of U0) -valued Function-like Function-yielding V36() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of U0 *), the carrier of U0)
PFuncs (( the carrier of U0 *), the carrier of U0) is non empty functional set
rng the charact of U0 is set
L is non empty Element of bool the carrier of U0
a is non empty Relation-like the carrier of U0 * -defined the carrier of U0 -valued Function-like homogeneous quasi_total Element of (U0)
(U0,L,a) is non empty Relation-like L * -defined L -valued Function-like homogeneous quasi_total Element of bool [:(L *),L:]

[:(L *),L:] is non empty set
bool [:(L *),L:] is non empty set
arity (U0,L,a) is V29() V30() V31() V35() V36() V41() Element of NAT
arity a is V29() V30() V31() V35() V36() V41() Element of NAT
() -tuples_on L is non empty functional FinSequence-membered FinSequenceSet of L
a | (() -tuples_on L) is Relation-like the carrier of U0 * -defined the carrier of U0 -valued Function-like Element of bool [:( the carrier of U0 *), the carrier of U0:]
[:( the carrier of U0 *), the carrier of U0:] is non empty set
bool [:( the carrier of U0 *), the carrier of U0:] is non empty set
dom (U0,L,a) is functional FinSequence-membered V89() set

(dom a) /\ (() -tuples_on L) is set
() -tuples_on the carrier of U0 is non empty functional FinSequence-membered FinSequenceSet of the carrier of U0
(() -tuples_on the carrier of U0) /\ (() -tuples_on L) is set
(arity (U0,L,a)) -tuples_on L is non empty functional FinSequence-membered FinSequenceSet of L
U0 is non empty V84() quasi_total non-empty UAStr
the carrier of U0 is non empty set
bool the carrier of U0 is non empty set
L is non empty V84() quasi_total non-empty UAStr
the carrier of L is non empty set
the charact of L is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of L *), the carrier of L) -valued Function-like Function-yielding V36() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of L *), the carrier of L)
the carrier of L * is non empty functional FinSequence-membered FinSequenceSet of the carrier of L
PFuncs (( the carrier of L *), the carrier of L) is non empty functional set
the charact of U0 is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of U0 *), the carrier of U0) -valued Function-like Function-yielding V36() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of U0 *), the carrier of U0)
the carrier of U0 * is non empty functional FinSequence-membered FinSequenceSet of the carrier of U0
PFuncs (( the carrier of U0 *), the carrier of U0) is non empty functional set
a is non empty Element of bool the carrier of U0
(U0,a) is Relation-like NAT -defined PFuncs ((a *),a) -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of PFuncs ((a *),a)

PFuncs ((a *),a) is non empty functional set
dom the charact of U0 is Element of bool NAT
dom (U0,a) is Element of bool NAT
b is V29() V30() V31() V35() V36() V41() set
the charact of U0 . b is homogeneous set
(U0,a) . b is set
(U0) is non empty PFuncsDomHQN of the carrier of U0
rng the charact of U0 is set
x is non empty Relation-like the carrier of U0 * -defined the carrier of U0 -valued Function-like homogeneous quasi_total Element of (U0)
(U0,a,x) is non empty Relation-like a * -defined a -valued Function-like homogeneous quasi_total Element of bool [:(a *),a:]
[:(a *),a:] is non empty set
bool [:(a *),a:] is non empty set
a is non empty Element of bool the carrier of U0
(U0,a) is Relation-like NAT -defined PFuncs ((a *),a) -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of PFuncs ((a *),a)

PFuncs ((a *),a) is non empty functional set
U0 is non empty V84() quasi_total non-empty UAStr
the carrier of U0 is non empty set
the charact of U0 is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of U0 *), the carrier of U0) -valued Function-like Function-yielding V36() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of U0 *), the carrier of U0)
the carrier of U0 * is non empty functional FinSequence-membered FinSequenceSet of the carrier of U0
PFuncs (( the carrier of U0 *), the carrier of U0) is non empty functional set
UAStr(# the carrier of U0, the charact of U0 #) is non empty strict UAStr
L is non empty strict V84() quasi_total non-empty UAStr
the carrier of L is non empty set
bool the carrier of U0 is non empty set
the charact of L is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of L *), the carrier of L) -valued Function-like Function-yielding V36() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of L *), the carrier of L)
the carrier of L * is non empty functional FinSequence-membered FinSequenceSet of the carrier of L
PFuncs (( the carrier of L *), the carrier of L) is non empty functional set
a is non empty Element of bool the carrier of U0
(U0,a) is Relation-like NAT -defined PFuncs ((a *),a) -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of PFuncs ((a *),a)

PFuncs ((a *),a) is non empty functional set
b is V29() V30() V31() V35() V36() V41() set
dom the charact of U0 is Element of bool NAT
(U0) is non empty PFuncsDomHQN of the carrier of U0
rng the charact of U0 is set
the charact of U0 . b is homogeneous set
dom (U0,a) is Element of bool NAT
(U0,a) . b is set
x is non empty Relation-like the carrier of U0 * -defined the carrier of U0 -valued Function-like homogeneous quasi_total Element of (U0)
(U0,a,x) is non empty Relation-like a * -defined a -valued Function-like homogeneous quasi_total Element of bool [:(a *),a:]
[:(a *),a:] is non empty set
bool [:(a *),a:] is non empty set
a is non empty V84() quasi_total non-empty (U0)
U0 is non empty V84() quasi_total non-empty UAStr
the carrier of U0 is non empty set
the carrier of U0 * is non empty functional FinSequence-membered FinSequenceSet of the carrier of U0
(U0) is non empty PFuncsDomHQN of the carrier of U0
the charact of U0 is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of U0 *), the carrier of U0) -valued Function-like Function-yielding V36() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of U0 *), the carrier of U0)
PFuncs (( the carrier of U0 *), the carrier of U0) is non empty functional set
rng the charact of U0 is set
L is non empty V84() quasi_total non-empty UAStr
the carrier of L is non empty set
the carrier of L * is non empty functional FinSequence-membered FinSequenceSet of the carrier of L
(L) is non empty PFuncsDomHQN of the carrier of L
the charact of L is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of L *), the carrier of L) -valued Function-like Function-yielding V36() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of L *), the carrier of L)
PFuncs (( the carrier of L *), the carrier of L) is non empty functional set
rng the charact of L is set
dom the charact of U0 is Element of bool NAT
a is non empty Relation-like the carrier of U0 * -defined the carrier of U0 -valued Function-like homogeneous quasi_total Element of (U0)
arity a is V29() V30() V31() V35() V36() V41() Element of NAT
b is non empty Relation-like the carrier of L * -defined the carrier of L -valued Function-like homogeneous quasi_total Element of (L)
arity b is V29() V30() V31() V35() V36() V41() Element of NAT
x is V29() V30() V31() V35() V36() V41() set
the charact of U0 . x is homogeneous set
the charact of L . x is homogeneous set
bool the carrier of L is non empty set
y is non empty Element of bool the carrier of L
(L,y) is Relation-like NAT -defined PFuncs ((y *),y) -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of PFuncs ((y *),y)

PFuncs ((y *),y) is non empty functional set
dom (L,y) is Element of bool NAT
(L,y) . x is set
(L,y,b) is non empty Relation-like y * -defined y -valued Function-like homogeneous quasi_total Element of bool [:(y *),y:]
[:(y *),y:] is non empty set
bool [:(y *),y:] is non empty set
() -tuples_on y is non empty functional FinSequence-membered FinSequenceSet of y
b | (() -tuples_on y) is Relation-like the carrier of L * -defined the carrier of L -valued Function-like Element of bool [:( the carrier of L *), the carrier of L:]
[:( the carrier of L *), the carrier of L:] is non empty set
bool [:( the carrier of L *), the carrier of L:] is non empty set

(dom b) /\ (() -tuples_on y) is set
() -tuples_on the carrier of L is non empty functional FinSequence-membered FinSequenceSet of the carrier of L
(() -tuples_on the carrier of L) /\ (() -tuples_on y) is set
() -tuples_on y is non empty functional FinSequence-membered FinSequenceSet of y
U0 is non empty V84() quasi_total non-empty UAStr
the charact of U0 is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of U0 *), the carrier of U0) -valued Function-like Function-yielding V36() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of U0 *), the carrier of U0)
the carrier of U0 is non empty set
the carrier of U0 * is non empty functional FinSequence-membered FinSequenceSet of the carrier of U0
PFuncs (( the carrier of U0 *), the carrier of U0) is non empty functional set
dom the charact of U0 is Element of bool NAT
L is non empty V84() quasi_total non-empty UAStr
the charact of L is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of L *), the carrier of L) -valued Function-like Function-yielding V36() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of L *), the carrier of L)
the carrier of L is non empty set
the carrier of L * is non empty functional FinSequence-membered FinSequenceSet of the carrier of L
PFuncs (( the carrier of L *), the carrier of L) is non empty functional set
dom the charact of L is Element of bool NAT
bool the carrier of L is non empty set
a is non empty Element of bool the carrier of L
(L,a) is Relation-like NAT -defined PFuncs ((a *),a) -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of PFuncs ((a *),a)

PFuncs ((a *),a) is non empty functional set
U0 is non empty V84() quasi_total non-empty UAStr
the carrier of U0 is non empty set
bool the carrier of U0 is non empty set
the charact of U0 is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of U0 *), the carrier of U0) -valued Function-like Function-yielding V36() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of U0 *), the carrier of U0)
the carrier of U0 * is non empty functional FinSequence-membered FinSequenceSet of the carrier of U0
PFuncs (( the carrier of U0 *), the carrier of U0) is non empty functional set
L is non empty Element of bool the carrier of U0
(U0,L) is Relation-like NAT -defined PFuncs ((L *),L) -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of PFuncs ((L *),L)

PFuncs ((L *),L) is non empty functional set
dom the charact of U0 is Element of bool NAT
dom (U0,L) is Element of bool NAT
a is V29() V30() V31() V35() V36() V41() set
the charact of U0 . a is homogeneous set
(U0,L) . a is set
(U0) is non empty PFuncsDomHQN of the carrier of U0
rng the charact of U0 is set
b is non empty Relation-like the carrier of U0 * -defined the carrier of U0 -valued Function-like homogeneous quasi_total Element of (U0)
(U0,L,b) is non empty Relation-like L * -defined L -valued Function-like homogeneous quasi_total Element of bool [:(L *),L:]
[:(L *),L:] is non empty set
bool [:(L *),L:] is non empty set
U0 is non empty V84() quasi_total non-empty UAStr
L is non empty V84() quasi_total non-empty UAStr
a is non empty V84() quasi_total non-empty UAStr
the carrier of U0 is non empty set
the carrier of L is non empty set
bool the carrier of L is non empty set
the carrier of a is non empty set
bool the carrier of a is non empty set
the charact of L is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of L *), the carrier of L) -valued Function-like Function-yielding V36() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of L *), the carrier of L)
the carrier of L * is non empty functional FinSequence-membered FinSequenceSet of the carrier of L
PFuncs (( the carrier of L *), the carrier of L) is non empty functional set
b is non empty Element of bool the carrier of a
(a,b) is Relation-like NAT -defined PFuncs ((b *),b) -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of PFuncs ((b *),b)

PFuncs ((b *),b) is non empty functional set
the charact of U0 is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of U0 *), the carrier of U0) -valued Function-like Function-yielding V36() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of U0 *), the carrier of U0)
the carrier of U0 * is non empty functional FinSequence-membered FinSequenceSet of the carrier of U0
PFuncs (( the carrier of U0 *), the carrier of U0) is non empty functional set
x is non empty Element of bool the carrier of a
(a,x) is Relation-like NAT -defined PFuncs ((x *),x) -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of PFuncs ((x *),x)

PFuncs ((x *),x) is non empty functional set
y is non empty Element of bool the carrier of L
(L,y) is Relation-like NAT -defined PFuncs ((y *),y) -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of PFuncs ((y *),y)

PFuncs ((y *),y) is non empty functional set
dom the charact of L is Element of bool NAT
dom (a,b) is Element of bool NAT
the charact of a is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of a *), the carrier of a) -valued Function-like Function-yielding V36() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of a *), the carrier of a)
the carrier of a * is non empty functional FinSequence-membered FinSequenceSet of the carrier of a
PFuncs (( the carrier of a *), the carrier of a) is non empty functional set
dom the charact of a is Element of bool NAT
(a) is non empty PFuncsDomHQN of the carrier of a
rng the charact of a is set
y is non empty Relation-like the carrier of a * -defined the carrier of a -valued Function-like homogeneous quasi_total Element of (a)
z is V29() V30() V31() V35() V36() V41() set
the charact of a . z is homogeneous set
(L) is non empty PFuncsDomHQN of the carrier of L
rng the charact of L is set
the charact of L . z is homogeneous set
u23 is non empty Relation-like the carrier of L * -defined the carrier of L -valued Function-like homogeneous quasi_total Element of (L)

arity u23 is V29() V30() V31() V35() V36() V41() Element of NAT
(arity u23) -tuples_on the carrier of L is non empty functional FinSequence-membered FinSequenceSet of the carrier of L
dom (L,y) is Element of bool NAT
(U0) is non empty PFuncsDomHQN of the carrier of U0
rng the charact of U0 is set
the charact of U0 . z is homogeneous set
u12 is non empty Relation-like the carrier of U0 * -defined the carrier of U0 -valued Function-like homogeneous quasi_total Element of (U0)

arity u12 is V29() V30() V31() V35() V36() V41() Element of NAT
(arity u12) -tuples_on the carrier of U0 is non empty functional FinSequence-membered FinSequenceSet of the carrier of U0

arity y is V29() V30() V31() V35() V36() V41() Element of NAT
() -tuples_on the carrier of a is non empty functional FinSequence-membered FinSequenceSet of the carrier of a
() -tuples_on b is non empty functional FinSequence-membered FinSequenceSet of b
y | (() -tuples_on b) is Relation-like the carrier of a * -defined the carrier of a -valued Function-like Element of bool [:( the carrier of a *), the carrier of a:]
[:( the carrier of a *), the carrier of a:] is non empty set
bool [:( the carrier of a *), the carrier of a:] is non empty set
dom (y | (() -tuples_on b)) is functional FinSequence-membered set
(dom y) /\ (() -tuples_on b) is set
(a,b,y) is non empty Relation-like b * -defined b -valued Function-like homogeneous quasi_total Element of bool [:(b *),b:]
[:(b *),b:] is non empty set
bool [:(b *),b:] is non empty set
(L,y,u23) is non empty Relation-like y * -defined y -valued Function-like homogeneous quasi_total Element of bool [:(y *),y:]
[:(y *),y:] is non empty set
bool [:(y *),y:] is non empty set
(arity u23) -tuples_on y is non empty functional FinSequence-membered FinSequenceSet of y
u23 | ((arity u23) -tuples_on y) is Relation-like the carrier of L * -defined the carrier of L -valued Function-like Element of bool [:( the carrier of L *), the carrier of L:]
[:( the carrier of L *), the carrier of L:] is non empty set
bool [:( the carrier of L *), the carrier of L:] is non empty set
(arity u12) -tuples_on y is non empty functional FinSequence-membered FinSequenceSet of y
((arity u23) -tuples_on the carrier of L) /\ ((arity u23) -tuples_on y) is set

rng u12 is set
rng C is set
len C is V29() V30() V31() V35() V36() V41() Element of NAT

{ } is set

{ b1 where b1 is Relation-like NAT -defined the carrier of U0 -valued Function-like V36() FinSequence-like FinSubsequence-like Element of the carrier of U0 * : len b1 = arity u12 } is set
u12 . o0 is set

{ } is set
(u23 | ((arity u23) -tuples_on y)) . B is set
u23 . B is set
(y | (() -tuples_on b)) . o1 is set
y . C is set
dom the charact of U0 is Element of bool NAT
dom (a,x) is Element of bool NAT
y is V29() V30() V31() V35() V36() V41() set
the charact of a . y is homogeneous set
the charact of L . y is homogeneous set
z is non empty Relation-like the carrier of a * -defined the carrier of a -valued Function-like homogeneous quasi_total Element of (a)
u23 is non empty Relation-like the carrier of L * -defined the carrier of L -valued Function-like homogeneous quasi_total Element of (L)
(a,x) . y is set
(a,x,z) is non empty Relation-like x * -defined x -valued Function-like homogeneous quasi_total Element of bool [:(x *),x:]
[:(x *),x:] is non empty set
bool [:(x *),x:] is non empty set
arity z is V29() V30() V31() V35() V36() V41() Element of NAT
() -tuples_on x is non empty functional FinSequence-membered FinSequenceSet of x
z | (() -tuples_on x) is Relation-like the carrier of a * -defined the carrier of a -valued Function-like Element of bool [:( the carrier of a *), the carrier of a:]
() -tuples_on b is non empty functional FinSequence-membered FinSequenceSet of b
(() -tuples_on b) /\ (() -tuples_on x) is set
z | ((() -tuples_on b) /\ (() -tuples_on x)) is Relation-like the carrier of a * -defined the carrier of a -valued Function-like Element of bool [:( the carrier of a *), the carrier of a:]
z | (() -tuples_on b) is Relation-like the carrier of a * -defined the carrier of a -valued Function-like Element of bool [:( the carrier of a *), the carrier of a:]
(z | (() -tuples_on b)) | (() -tuples_on x) is Relation-like the carrier of a * -defined the carrier of a -valued Function-like Element of bool [:( the carrier of a *), the carrier of a:]
(a,b,z) is non empty Relation-like b * -defined b -valued Function-like homogeneous quasi_total Element of bool [:(b *),b:]
(a,b,z) | (() -tuples_on x) is Relation-like b * -defined b -valued Function-like Element of bool [:(b *),b:]
u23 | (() -tuples_on x) is Relation-like the carrier of L * -defined the carrier of L -valued Function-like Element of bool [:( the carrier of L *), the carrier of L:]
arity u23 is V29() V30() V31() V35() V36() V41() Element of NAT
(arity u23) -tuples_on y is non empty functional FinSequence-membered FinSequenceSet of y
u23 | ((arity u23) -tuples_on y) is Relation-like the carrier of L * -defined the carrier of L -valued Function-like Element of bool [:( the carrier of L *), the carrier of L:]
(L,y,u23) is non empty Relation-like y * -defined y -valued Function-like homogeneous quasi_total Element of bool [:(y *),y:]
the charact of U0 . y is homogeneous set
U0 is non empty V84() quasi_total non-empty UAStr
L is non empty V84() quasi_total non-empty UAStr
the carrier of L is non empty set
bool the carrier of L is non empty set
the carrier of U0 is non empty set
b is non empty Element of bool the carrier of L
(L,b) is Relation-like NAT -defined PFuncs ((b *),b) -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of PFuncs ((b *),b)

PFuncs ((b *),b) is non empty functional set
dom (L,b) is Element of bool NAT
the charact of L is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of L *), the carrier of L) -valued Function-like Function-yielding V36() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of L *), the carrier of L)
the carrier of L * is non empty functional FinSequence-membered FinSequenceSet of the carrier of L
PFuncs (( the carrier of L *), the carrier of L) is non empty functional set
dom the charact of L is Element of bool NAT
x is V29() V30() V31() V35() V36() V41() set
the charact of L . x is homogeneous set
(L,b) . x is set
(L) is non empty PFuncsDomHQN of the carrier of L
rng the charact of L is set
y is non empty Relation-like the carrier of L * -defined the carrier of L -valued Function-like homogeneous quasi_total Element of (L)
(L,b,y) is non empty Relation-like b * -defined b -valued Function-like homogeneous quasi_total Element of bool [:(b *),b:]
[:(b *),b:] is non empty set
bool [:(b *),b:] is non empty set
bool the carrier of U0 is non empty set
a is non empty Element of bool the carrier of L
the charact of U0 is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of U0 *), the carrier of U0) -valued Function-like Function-yielding V36() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of U0 *), the carrier of U0)
the carrier of U0 * is non empty functional FinSequence-membered FinSequenceSet of the carrier of U0
PFuncs (( the carrier of U0 *), the carrier of U0) is non empty functional set
U0 is non empty V84() quasi_total non-empty UAStr
L is non empty V84() quasi_total non-empty (U0)
the carrier of L is non empty set
a is non empty V84() quasi_total non-empty (U0)
the carrier of a is non empty set
the charact of L is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of L *), the carrier of L) -valued Function-like Function-yielding V36() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of L *), the carrier of L)
the carrier of L * is non empty functional FinSequence-membered FinSequenceSet of the carrier of L
PFuncs (( the carrier of L *), the carrier of L) is non empty functional set
dom the charact of L is Element of bool NAT
the charact of U0 is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of U0 *), the carrier of U0) -valued Function-like Function-yielding V36() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of U0 *), the carrier of U0)
the carrier of U0 is non empty set
the carrier of U0 * is non empty functional FinSequence-membered FinSequenceSet of the carrier of U0
PFuncs (( the carrier of U0 *), the carrier of U0) is non empty functional set
dom the charact of U0 is Element of bool NAT
bool the carrier of U0 is non empty set
bool the carrier of a is non empty set
x is non empty Element of bool the carrier of a
(a,x) is Relation-like NAT -defined PFuncs ((x *),x) -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of PFuncs ((x *),x)

PFuncs ((x *),x) is non empty functional set
the charact of a is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of a *), the carrier of a) -valued Function-like Function-yielding V36() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of a *), the carrier of a)
the carrier of a * is non empty functional FinSequence-membered FinSequenceSet of the carrier of a
PFuncs (( the carrier of a *), the carrier of a) is non empty functional set
y is non empty Element of bool the carrier of U0
(U0,y) is Relation-like NAT -defined PFuncs ((y *),y) -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of PFuncs ((y *),y)

PFuncs ((y *),y) is non empty functional set
dom (a,x) is Element of bool NAT
dom the charact of a is Element of bool NAT
b is non empty Element of bool the carrier of U0
(a) is non empty PFuncsDomHQN of the carrier of a
rng the charact of a is set
y is non empty Relation-like the carrier of a * -defined the carrier of a -valued Function-like homogeneous quasi_total Element of (a)

len z is V29() V30() V31() V35() V36() V41() Element of NAT
arity y is V29() V30() V31() V35() V36() V41() Element of NAT
y . z is set
u23 is V29() V30() V31() V35() V36() V41() set
the charact of a . u23 is homogeneous set
(U0) is non empty PFuncsDomHQN of the carrier of U0
rng the charact of U0 is set
the charact of U0 . u23 is homogeneous set
u12 is non empty Relation-like the carrier of U0 * -defined the carrier of U0 -valued Function-like homogeneous quasi_total Element of (U0)
arity u12 is V29() V30() V31() V35() V36() V41() Element of NAT
rng z is set

(arity u12) -tuples_on y is non empty functional FinSequence-membered FinSequenceSet of y
(U0,y,u12) is non empty Relation-like y * -defined y -valued Function-like homogeneous quasi_total Element of bool [:(y *),y:]
[:(y *),y:] is non empty set
bool [:(y *),y:] is non empty set
u12 | ((arity u12) -tuples_on y) is Relation-like the carrier of U0 * -defined the carrier of U0 -valued Function-like Element of bool [:( the carrier of U0 *), the carrier of U0:]
[:( the carrier of U0 *), the carrier of U0:] is non empty set
bool [:( the carrier of U0 *), the carrier of U0:] is non empty set
{ } is set

u12 . B is set
(U0,b) is Relation-like NAT -defined PFuncs ((b *),b) -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of PFuncs ((b *),b)

PFuncs ((b *),b) is non empty functional set
y is V29() V30() V31() V35() V36() V41() set
(U0) is non empty PFuncsDomHQN of the carrier of U0
rng the charact of U0 is set
the charact of U0 . y is homogeneous set
(a) is non empty PFuncsDomHQN of the carrier of a
rng the charact of a is set
the charact of a . y is homogeneous set
u23 is non empty Relation-like the carrier of a * -defined the carrier of a -valued Function-like homogeneous quasi_total Element of (a)
z is non empty Relation-like the carrier of U0 * -defined the carrier of U0 -valued Function-like homogeneous quasi_total Element of (U0)
(U0,y,z) is non empty Relation-like y * -defined y -valued Function-like homogeneous quasi_total Element of bool [:(y *),y:]
[:(y *),y:] is non empty set
bool [:(y *),y:] is non empty set
arity u23 is V29() V30() V31() V35() V36() V41() Element of NAT
arity z is V29() V30() V31() V35() V36() V41() Element of NAT
the charact of L . y is homogeneous set
(U0,b,z) is non empty Relation-like b * -defined b -valued Function-like homogeneous quasi_total Element of bool [:(b *),b:]
[:(b *),b:] is non empty set
bool [:(b *),b:] is non empty set
() -tuples_on b is non empty functional FinSequence-membered FinSequenceSet of b
z | (() -tuples_on b) is Relation-like the carrier of U0 * -defined the carrier of U0 -valued Function-like Element of bool [:( the carrier of U0 *), the carrier of U0:]
[:( the carrier of U0 *), the carrier of U0:] is non empty set
bool [:( the carrier of U0 *), the carrier of U0:] is non empty set
() -tuples_on y is non empty functional FinSequence-membered FinSequenceSet of y
(() -tuples_on y) /\ (() -tuples_on b) is set
z | ((() -tuples_on y) /\ (() -tuples_on b)) is Relation-like the carrier of U0 * -defined the carrier of U0 -valued Function-like Element of bool [:( the carrier of U0 *), the carrier of U0:]
z | (() -tuples_on y) is Relation-like the carrier of U0 * -defined the carrier of U0 -valued Function-like Element of bool [:( the carrier of U0 *), the carrier of U0:]
() -tuples_on x is non empty functional FinSequence-membered FinSequenceSet of x
(z | (() -tuples_on y)) | (() -tuples_on x) is Relation-like the carrier of U0 * -defined the carrier of U0 -valued Function-like Element of bool [:( the carrier of U0 *), the carrier of U0:]
(U0,y,z) | (() -tuples_on x) is Relation-like y * -defined y -valued Function-like Element of bool [:(y *),y:]
(a,x,u23) is non empty Relation-like x * -defined x -valued Function-like homogeneous quasi_total Element of bool [:(x *),x:]
[:(x *),x:] is non empty set
bool [:(x *),x:] is non empty set
(a,x) . y is set
U0 is non empty V84() quasi_total non-empty UAStr
L is non empty strict V84() quasi_total non-empty (U0)
the carrier of L is non empty set
a is non empty strict V84() quasi_total non-empty (U0)
the carrier of a is non empty set
U0 is non empty V84() quasi_total non-empty UAStr
L is non empty V84() quasi_total non-empty UAStr

dom () is Element of bool NAT
len () is V29() V30() V31() V35() V36() V41() Element of NAT
the charact of U0 is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of U0 *), the carrier of U0) -valued Function-like Function-yielding V36() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of U0 *), the carrier of U0)
the carrier of U0 is non empty set
the carrier of U0 * is non empty functional FinSequence-membered FinSequenceSet of the carrier of U0
PFuncs (( the carrier of U0 *), the carrier of U0) is non empty functional set
len the charact of U0 is non empty V29() V30() V31() V35() V36() V41() Element of NAT
dom the charact of U0 is Element of bool NAT
the carrier of L is non empty set
bool the carrier of L is non empty set
len () is V29() V30() V31() V35() V36() V41() Element of NAT
the charact of L is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of L *), the carrier of L) -valued Function-like Function-yielding V36() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of L *), the carrier of L)
the carrier of L * is non empty functional FinSequence-membered FinSequenceSet of the carrier of L
PFuncs (( the carrier of L *), the carrier of L) is non empty functional set
len the charact of L is non empty V29() V30() V31() V35() V36() V41() Element of NAT
dom () is Element of bool NAT
dom the charact of L is Element of bool NAT
y is non empty Element of bool the carrier of L
(L,y) is Relation-like NAT -defined PFuncs ((y *),y) -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of PFuncs ((y *),y)

PFuncs ((y *),y) is non empty functional set
dom (L,y) is Element of bool NAT
y is V29() V30() V31() V35() V36() V41() set
() . y is set
() . y is set
(U0) is non empty PFuncsDomHQN of the carrier of U0
rng the charact of U0 is set
the charact of U0 . y is homogeneous set
(L) is non empty PFuncsDomHQN of the carrier of L
rng the charact of L is set
the charact of L . y is homogeneous set
z is non empty Relation-like the carrier of U0 * -defined the carrier of U0 -valued Function-like homogeneous quasi_total Element of (U0)
arity z is V29() V30() V31() V35() V36() V41() Element of NAT
u23 is non empty Relation-like the carrier of L * -defined the carrier of L -valued Function-like homogeneous quasi_total Element of (L)
arity u23 is V29() V30() V31() V35() V36() V41() Element of NAT
U0 is non empty V84() quasi_total non-empty UAStr
the carrier of U0 is non empty set
bool the carrier of U0 is non empty set
L is non empty Element of bool the carrier of U0
(U0,L) is Relation-like NAT -defined PFuncs ((L *),L) -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of PFuncs ((L *),L)

PFuncs ((L *),L) is non empty functional set
UAStr(# L,(U0,L) #) is non empty strict UAStr
the charact of UAStr(# L,(U0,L) #) is Relation-like NAT -defined PFuncs (( the carrier of UAStr(# L,(U0,L) #) *), the carrier of UAStr(# L,(U0,L) #)) -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of PFuncs (( the carrier of UAStr(# L,(U0,L) #) *), the carrier of UAStr(# L,(U0,L) #))
the carrier of UAStr(# L,(U0,L) #) is non empty set
the carrier of UAStr(# L,(U0,L) #) * is non empty functional FinSequence-membered FinSequenceSet of the carrier of UAStr(# L,(U0,L) #)
PFuncs (( the carrier of UAStr(# L,(U0,L) #) *), the carrier of UAStr(# L,(U0,L) #)) is non empty functional set
dom the charact of UAStr(# L,(U0,L) #) is Element of bool NAT
the charact of U0 is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of U0 *), the carrier of U0) -valued Function-like Function-yielding V36() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of U0 *), the carrier of U0)
the carrier of U0 * is non empty functional FinSequence-membered FinSequenceSet of the carrier of U0
PFuncs (( the carrier of U0 *), the carrier of U0) is non empty functional set
dom the charact of U0 is Element of bool NAT
b is set
the charact of UAStr(# L,(U0,L) #) . b is set
(U0) is non empty PFuncsDomHQN of the carrier of U0
rng the charact of U0 is set
the charact of U0 . b is homogeneous set
x is non empty Relation-like the carrier of U0 * -defined the carrier of U0 -valued Function-like homogeneous quasi_total Element of (U0)
(U0,L,x) is non empty Relation-like L * -defined L -valued Function-like homogeneous quasi_total Element of bool [:(L *),L:]
[:(L *),L:] is non empty set
bool [:(L *),L:] is non empty set
[:( the carrier of UAStr(# L,(U0,L) #) *), the carrier of UAStr(# L,(U0,L) #):] is non empty set
bool [:( the carrier of UAStr(# L,(U0,L) #) *), the carrier of UAStr(# L,(U0,L) #):] is non empty set
b is V29() V30() V31() V35() V36() V41() set
the charact of UAStr(# L,(U0,L) #) . b is set
x is Relation-like the carrier of UAStr(# L,(U0,L) #) * -defined the carrier of UAStr(# L,(U0,L) #) -valued Function-like Element of bool [:( the carrier of UAStr(# L,(U0,L) #) *), the carrier of UAStr(# L,(U0,L) #):]
(U0) is non empty PFuncsDomHQN of the carrier of U0
rng the charact of U0 is set
the charact of U0 . b is homogeneous set
y is non empty Relation-like the carrier of U0 * -defined the carrier of U0 -valued Function-like homogeneous quasi_total Element of (U0)
(U0,L,y) is non empty Relation-like L * -defined L -valued Function-like homogeneous quasi_total Element of bool [:(L *),L:]
[:(L *),L:] is non empty set
bool [:(L *),L:] is non empty set
b is V29() V30() V31() V35() V36() V41() set
the charact of UAStr(# L,(U0,L) #) . b is set
x is Relation-like the carrier of UAStr(# L,(U0,L) #) * -defined the carrier of UAStr(# L,(U0,L) #) -valued Function-like Element of bool [:( the carrier of UAStr(# L,(U0,L) #) *), the carrier of UAStr(# L,(U0,L) #):]
(U0) is non empty PFuncsDomHQN of the carrier of U0
rng the charact of U0 is set
the charact of U0 . b is homogeneous set
y is non empty Relation-like the carrier of U0 * -defined the carrier of U0 -valued Function-like homogeneous quasi_total Element of (U0)
(U0,L,y) is non empty Relation-like L * -defined L -valued Function-like homogeneous quasi_total Element of bool [:(L *),L:]
[:(L *),L:] is non empty set
bool [:(L *),L:] is non empty set
U0 is non empty V84() quasi_total non-empty UAStr
the carrier of U0 is non empty set
bool the carrier of U0 is non empty set
L is non empty Element of bool the carrier of U0
(U0,L) is Relation-like NAT -defined PFuncs ((L *),L) -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of PFuncs ((L *),L)

PFuncs ((L *),L) is non empty functional set
UAStr(# L,(U0,L) #) is non empty strict UAStr
a is non empty strict V84() quasi_total non-empty UAStr
the carrier of a is non empty set
the charact of a is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of a *), the carrier of a) -valued Function-like Function-yielding V36() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of a *), the carrier of a)
the carrier of a * is non empty functional FinSequence-membered FinSequenceSet of the carrier of a
PFuncs (( the carrier of a *), the carrier of a) is non empty functional set
b is non empty Element of bool the carrier of U0
(U0,b) is Relation-like NAT -defined PFuncs ((b *),b) -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of PFuncs ((b *),b)

PFuncs ((b *),b) is non empty functional set
U0 is non empty V84() quasi_total non-empty UAStr
L is non empty V84() quasi_total non-empty (U0)
the carrier of L is non empty set
a is non empty V84() quasi_total non-empty (U0)
the carrier of a is non empty set
the carrier of L /\ the carrier of a is set
the carrier of U0 is non empty set
bool the carrier of U0 is non empty set
b is non empty Element of bool the carrier of U0
(U0,b) is Relation-like NAT -defined PFuncs ((b *),b) -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of PFuncs ((b *),b)

PFuncs ((b *),b) is non empty functional set
UAStr(# b,(U0,b) #) is non empty strict UAStr
the carrier of U0 * is non empty functional FinSequence-membered FinSequenceSet of the carrier of U0
(U0) is non empty PFuncsDomHQN of the carrier of U0
the charact of U0 is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of U0 *), the carrier of U0) -valued Function-like Function-yielding V36() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of U0 *), the carrier of U0)
PFuncs (( the carrier of U0 *), the carrier of U0) is non empty functional set
rng the charact of U0 is set

len u23 is V29() V30() V31() V35() V36() V41() Element of NAT
y is non empty Relation-like the carrier of U0 * -defined the carrier of U0 -valued Function-like homogeneous quasi_total Element of (U0)
arity y is V29() V30() V31() V35() V36() V41() Element of NAT
o0 is non empty Element of bool the carrier of U0

y . u12 is set
B is non empty Element of bool the carrier of U0

y . C is set
y . u23 is set
the carrier of UAStr(# b,(U0,b) #) is non empty set
the charact of UAStr(# b,(U0,b) #) is Relation-like NAT -defined PFuncs (( the carrier of UAStr(# b,(U0,b) #) *), the carrier of UAStr(# b,(U0,b) #)) -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of PFuncs (( the carrier of UAStr(# b,(U0,b) #) *), the carrier of UAStr(# b,(U0,b) #))
the carrier of UAStr(# b,(U0,b) #) * is non empty functional FinSequence-membered FinSequenceSet of the carrier of UAStr(# b,(U0,b) #)
PFuncs (( the carrier of UAStr(# b,(U0,b) #) *), the carrier of UAStr(# b,(U0,b) #)) is non empty functional set
y is non empty Element of bool the carrier of U0
(U0,y) is Relation-like NAT -defined PFuncs ((y *),y) -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of PFuncs ((y *),y)

PFuncs ((y *),y) is non empty functional set
y is non empty V84() quasi_total non-empty UAStr
y is non empty strict V84() quasi_total non-empty (U0)
the carrier of y is non empty set
the charact of y is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of y *), the carrier of y) -valued Function-like Function-yielding V36() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of y *), the carrier of y)
the carrier of y * is non empty functional FinSequence-membered FinSequenceSet of the carrier of y
PFuncs (( the carrier of y *), the carrier of y) is non empty functional set
z is non empty Element of bool the carrier of U0
(U0,z) is Relation-like NAT -defined PFuncs ((z *),z) -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of PFuncs ((z *),z)

PFuncs ((z *),z) is non empty functional set
x is non empty strict V84() quasi_total non-empty (U0)
the carrier of x is non empty set
the charact of x is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of x *), the carrier of x) -valued Function-like Function-yielding V36() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of x *), the carrier of x)
the carrier of x * is non empty functional FinSequence-membered FinSequenceSet of the carrier of x
PFuncs (( the carrier of x *), the carrier of x) is non empty functional set
y is non empty strict V84() quasi_total non-empty (U0)
the carrier of y is non empty set
the charact of y is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of y *), the carrier of y) -valued Function-like Function-yielding V36() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of y *), the carrier of y)
the carrier of y * is non empty functional FinSequence-membered FinSequenceSet of the carrier of y
PFuncs (( the carrier of y *), the carrier of y) is non empty functional set
b is non empty Element of bool the carrier of U0
(U0,b) is Relation-like NAT -defined PFuncs ((b *),b) -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of PFuncs ((b *),b)

PFuncs ((b *),b) is non empty functional set
U0 is non empty V84() quasi_total non-empty UAStr
the carrier of U0 is non empty set
the carrier of U0 * is non empty functional FinSequence-membered FinSequenceSet of the carrier of U0
(U0) is non empty PFuncsDomHQN of the carrier of U0
the charact of U0 is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of U0 *), the carrier of U0) -valued Function-like Function-yielding V36() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of U0 *), the carrier of U0)
PFuncs (( the carrier of U0 *), the carrier of U0) is non empty functional set
rng the charact of U0 is set
{ b1 where b1 is Element of the carrier of U0 : ex b2 being non empty Relation-like the carrier of U0 * -defined the carrier of U0 -valued Function-like homogeneous quasi_total Element of (U0) st
( arity b2 = 0 & b1 in rng b2 )
}
is set

bool the carrier of U0 is non empty set
a is set
b is Element of the carrier of U0
x is non empty Relation-like the carrier of U0 * -defined the carrier of U0 -valued Function-like homogeneous quasi_total Element of (U0)
arity x is V29() V30() V31() V35() V36() V41() Element of NAT
rng x is set
the non empty set is non empty set
the Element of the non empty set is Element of the non empty set
the non empty set * is non empty functional FinSequence-membered FinSequenceSet of the non empty set
PFuncs (( the non empty set *), the non empty set ) is non empty functional set
<*> the non empty set is empty proper Relation-like NAT -defined the non empty set -valued Function-like functional V29() V30() V31() V33() V34() V35() V36() V41() V43( {} ) FinSequence-like FinSubsequence-like FinSequence-membered V89() FinSequence of the non empty set
[:NAT, the non empty set :] is non empty V36() set
(<*> the non empty set ) .--> the Element of the non empty set is set
{(<*> the non empty set )} is non empty trivial V43(1) set
{(<*> the non empty set )} --> the Element of the non empty set is Relation-like {(<*> the non empty set )} -defined { the Element of the non empty set } -valued Function-like V21({(<*> the non empty set )},{ the Element of the non empty set }) Element of bool [:{(<*> the non empty set )},{ the Element of the non empty set }:]
{ the Element of the non empty set } is non empty trivial V43(1) set
[:{(<*> the non empty set )},{ the Element of the non empty set }:] is non empty set
bool [:{(<*> the non empty set )},{ the Element of the non empty set }:] is non empty set
a is Element of PFuncs (( the non empty set *), the non empty set )
<*a*> is non empty trivial Relation-like NAT -defined PFuncs (( the non empty set *), the non empty set ) -valued Function-like V36() V43(1) FinSequence-like FinSubsequence-like FinSequence of PFuncs (( the non empty set *), the non empty set )
UAStr(# the non empty set ,<*a*> #) is non empty strict UAStr
the carrier of UAStr(# the non empty set ,<*a*> #) is non empty set
the charact of UAStr(# the non empty set ,<*a*> #) is Relation-like NAT -defined PFuncs (( the carrier of UAStr(# the non empty set ,<*a*> #) *), the carrier of UAStr(# the non empty set ,<*a*> #)) -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of PFuncs (( the carrier of UAStr(# the non empty set ,<*a*> #) *), the carrier of UAStr(# the non empty set ,<*a*> #))
the carrier of UAStr(# the non empty set ,<*a*> #) * is non empty functional FinSequence-membered FinSequenceSet of the carrier of UAStr(# the non empty set ,<*a*> #)
PFuncs (( the carrier of UAStr(# the non empty set ,<*a*> #) *), the carrier of UAStr(# the non empty set ,<*a*> #)) is non empty functional set
x is non empty V84() quasi_total non-empty UAStr

the carrier of x is non empty set
the carrier of x * is non empty functional FinSequence-membered FinSequenceSet of the carrier of x
(x) is non empty PFuncsDomHQN of the carrier of x
the charact of x is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of x *), the carrier of x) -valued Function-like Function-yielding V36() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of x *), the carrier of x)
PFuncs (( the carrier of x *), the carrier of x) is non empty functional set
rng the charact of x is set
the charact of x . 1 is homogeneous set
y is non empty Relation-like the carrier of x * -defined the carrier of x -valued Function-like homogeneous quasi_total Element of (x)

len y is V29() V30() V31() V35() V36() V41() Element of NAT
arity y is V29() V30() V31() V35() V36() V41() Element of NAT
U0 is non empty V84() quasi_total non-empty () UAStr
(U0) is Element of bool the carrier of U0
the carrier of U0 is non empty set
bool the carrier of U0 is non empty set
the carrier of U0 * is non empty functional FinSequence-membered FinSequenceSet of the carrier of U0
(U0) is non empty PFuncsDomHQN of the carrier of U0
the charact of U0 is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of U0 *), the carrier of U0) -valued Function-like Function-yielding V36() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of U0 *), the carrier of U0)
PFuncs (( the carrier of U0 *), the carrier of U0) is non empty functional set
rng the charact of U0 is set
{ b1 where b1 is Element of the carrier of U0 : ex b2 being non empty Relation-like the carrier of U0 * -defined the carrier of U0 -valued Function-like homogeneous quasi_total Element of (U0) st
( arity b2 = 0 & b1 in rng b2 )
}
is set

L is non empty Relation-like the carrier of U0 * -defined the carrier of U0 -valued Function-like homogeneous quasi_total Element of (U0)
arity L is V29() V30() V31() V35() V36() V41() Element of NAT

0 -tuples_on the carrier of U0 is non empty functional FinSequence-membered FinSequenceSet of the carrier of U0
<*> the carrier of U0 is empty proper Relation-like NAT -defined the carrier of U0 -valued Function-like functional V29() V30() V31() V33() V34() V35() V36() V41() V43( {} ) FinSequence-like FinSubsequence-like FinSequence-membered V89() FinSequence of the carrier of U0
[:NAT, the carrier of U0:] is non empty V36() set
{(<*> the carrier of U0)} is non empty trivial V43(1) set
L . (<*> the carrier of U0) is set
rng L is set
a is Element of the carrier of U0
U0 is non empty V84() quasi_total non-empty UAStr
(U0) is Element of bool the carrier of U0
the carrier of U0 is non empty set
bool the carrier of U0 is non empty set
the carrier of U0 * is non empty functional FinSequence-membered FinSequenceSet of the carrier of U0
(U0) is non empty PFuncsDomHQN of the carrier of U0
the charact of U0 is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of U0 *), the carrier of U0) -valued Function-like Function-yielding V36() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of U0 *), the carrier of U0)
PFuncs (( the carrier of U0 *), the carrier of U0) is non empty functional set
rng the charact of U0 is set
{ b1 where b1 is Element of the carrier of U0 : ex b2 being non empty Relation-like the carrier of U0 * -defined the carrier of U0 -valued Function-like homogeneous quasi_total Element of (U0) st
( arity b2 = 0 & b1 in rng b2 )
}
is set

L is non empty V84() quasi_total non-empty (U0)
the carrier of L is non empty set
bool the carrier of L is non empty set
x is set
y is Element of the carrier of U0
y is non empty Relation-like the carrier of U0 * -defined the carrier of U0 -valued Function-like homogeneous quasi_total Element of (U0)
arity y is V29() V30() V31() V35() V36() V41() Element of NAT
rng y is set
y is non empty Relation-like the carrier of U0 * -defined the carrier of U0 -valued Function-like homogeneous quasi_total Element of (U0)
arity y is V29() V30() V31() V35() V36() V41() Element of NAT
rng y is set

z is set
y . z is set
0 -tuples_on the carrier of U0 is non empty functional FinSequence-membered FinSequenceSet of the carrier of U0
<*> the carrier of U0 is empty proper Relation-like NAT -defined the carrier of U0 -valued Function-like functional V29() V30() V31() V33() V34() V35() V36() V41() V43( {} ) FinSequence-like FinSubsequence-like FinSequence-membered V89() FinSequence of the carrier of U0
[:NAT, the carrier of U0:] is non empty V36() set
{(<*> the carrier of U0)} is non empty trivial V43(1) set
b is non empty Element of bool the carrier of U0

[:NAT,b:] is non empty V36() set
{(<*> b)} is non empty trivial V43(1) set

() -tuples_on b is non empty functional FinSequence-membered FinSequenceSet of b
(dom y) /\ (() -tuples_on b) is set
y | (() -tuples_on b) is Relation-like the carrier of U0 * -defined the carrier of U0 -valued Function-like Element of bool [:( the carrier of U0 *), the carrier of U0:]
[:( the carrier of U0 *), the carrier of U0:] is non empty set
bool [:( the carrier of U0 *), the carrier of U0:] is non empty set
dom (y | (() -tuples_on b)) is functional FinSequence-membered set
dom the charact of U0 is Element of bool NAT
u23 is V29() V30() V31() V35() V36() V41() set
the charact of U0 . u23 is homogeneous set
the charact of L is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of L *), the carrier of L) -valued Function-like Function-yielding V36() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of L *), the carrier of L)
the carrier of L * is non empty functional FinSequence-membered FinSequenceSet of the carrier of L
PFuncs (( the carrier of L *), the carrier of L) is non empty functional set
dom the charact of L is Element of bool NAT
(L) is non empty PFuncsDomHQN of the carrier of L
rng the charact of L is set
the charact of L . u23 is homogeneous set
(U0,b) is Relation-like NAT -defined PFuncs ((b *),b) -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of PFuncs ((b *),b)

PFuncs ((b *),b) is non empty functional set
u12 is non empty Relation-like the carrier of L * -defined the carrier of L -valued Function-like homogeneous quasi_total Element of (L)
(U0,b,y) is non empty Relation-like b * -defined b -valued Function-like homogeneous quasi_total Element of bool [:(b *),b:]
[:(b *),b:] is non empty set
bool [:(b *),b:] is non empty set
dom (U0,b,y) is functional FinSequence-membered V89() set
u12 . z is set
rng u12 is set
(y | (() -tuples_on b)) . z is set
U0 is non empty V84() quasi_total non-empty () UAStr
(U0) is non empty Element of bool the carrier of U0
the carrier of U0 is non empty set
bool the carrier of U0 is non empty set
the carrier of U0 * is non empty functional FinSequence-membered FinSequenceSet of the carrier of U0
(U0) is non empty PFuncsDomHQN of the carrier of U0
the charact of U0 is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of U0 *), the carrier of U0) -valued Function-like Function-yielding V36() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of U0 *), the carrier of U0)
PFuncs (( the carrier of U0 *), the carrier of U0) is non empty functional set
rng the charact of U0 is set
{ b1 where