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
signature a is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of NAT
b is non empty V84() quasi_total non-empty UAStr
signature b is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of NAT
a is non empty V84() quasi_total non-empty UAStr
signature a is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of NAT
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
signature U0 is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of NAT
len (signature U0) is V29() V30() V31() V35() V36() V41() Element of NAT
signature L is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of NAT
len (signature L) 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
signature U0 is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of NAT
signature L is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of NAT
signature a is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of NAT
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
(arity a) -tuples_on L is non empty functional FinSequence-membered FinSequenceSet of L
a | ((arity 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 * is non empty functional FinSequence-membered FinSequenceSet of L
[:(L *),L:] is non empty set
bool [:(L *),L:] is non empty set
(arity a) -tuples_on the carrier of U0 is non empty functional FinSequence-membered FinSequenceSet of the carrier of U0
b is set
{ b1 where b1 is Relation-like NAT -defined L -valued Function-like V36() FinSequence-like FinSubsequence-like Element of L * : len b1 = arity a } is set
x is Relation-like NAT -defined L -valued Function-like V36() FinSequence-like FinSubsequence-like Element of L *
len x is V29() V30() V31() V35() V36() V41() Element of NAT
rng x is set
y is Relation-like NAT -defined the carrier of U0 -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of the carrier of U0
y is Relation-like NAT -defined the carrier of U0 -valued Function-like V36() FinSequence-like FinSubsequence-like Element of the carrier of U0 *
{ 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 | ((arity a) -tuples_on L)) is functional FinSequence-membered set
dom a is functional FinSequence-membered V89() set
(dom a) /\ ((arity a) -tuples_on L) is set
((arity a) -tuples_on the carrier of U0) /\ ((arity a) -tuples_on L) is set
rng (a | ((arity a) -tuples_on L)) is set
b is set
x is set
(a | ((arity a) -tuples_on L)) . x is set
{ b1 where b1 is Relation-like NAT -defined L -valued Function-like V36() FinSequence-like FinSubsequence-like Element of L * : len b1 = arity a } is set
y is Relation-like NAT -defined L -valued Function-like V36() FinSequence-like FinSubsequence-like Element of L *
len y is V29() V30() V31() V35() V36() V41() Element of NAT
(a | ((arity 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
b is Relation-like L * -defined L -valued Function-like Element of bool [:(L *),L:]
x is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like set
dom b is functional FinSequence-membered set
y is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like 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
{ b1 where b1 is Relation-like NAT -defined L -valued Function-like V36() FinSequence-like FinSubsequence-like Element of L * : len b1 = arity a } is set
y is Relation-like NAT -defined L -valued Function-like V36() FinSequence-like FinSubsequence-like Element of L *
len y is V29() V30() V31() V35() V36() V41() Element of NAT
z is Relation-like NAT -defined L -valued Function-like V36() FinSequence-like FinSubsequence-like Element of L *
len z is V29() V30() V31() V35() V36() V41() Element of NAT
x is Relation-like NAT -defined L -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of L
len x is V29() V30() V31() V35() V36() V41() Element of NAT
dom b is functional FinSequence-membered set
y is Relation-like NAT -defined L -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of L
len y is V29() V30() V31() V35() V36() V41() Element of NAT
{ b1 where b1 is Relation-like NAT -defined L -valued Function-like V36() FinSequence-like FinSubsequence-like Element of L * : len b1 = arity a } is set
y is Relation-like NAT -defined L -valued Function-like V36() FinSequence-like FinSubsequence-like Element of L *
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
L * is non empty functional FinSequence-membered FinSequenceSet of L
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:]
a is Relation-like NAT -defined PFuncs ((L *),L) -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of PFuncs ((L *),L)
dom a is Element of bool NAT
b is Relation-like NAT -defined PFuncs ((L *),L) -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of PFuncs ((L *),L)
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
a is Relation-like NAT -defined PFuncs ((L *),L) -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of PFuncs ((L *),L)
dom a is Element of bool NAT
b is Relation-like NAT -defined PFuncs ((L *),L) -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of PFuncs ((L *),L)
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)
b is Relation-like NAT -defined L -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of L
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
dom a is functional FinSequence-membered V89() set
(arity a) -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 * is non empty functional FinSequence-membered FinSequenceSet of L
[:(L *),L:] is non empty set
bool [:(L *),L:] is non empty set
dom a is functional FinSequence-membered V89() set
arity a is V29() V30() V31() V35() V36() V41() Element of NAT
(arity a) -tuples_on L is non empty functional FinSequence-membered FinSequenceSet of L
a | ((arity 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 * is non empty functional FinSequence-membered FinSequenceSet of 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 * is non empty functional FinSequence-membered FinSequenceSet of 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
(arity a) -tuples_on L is non empty functional FinSequence-membered FinSequenceSet of L
a | ((arity 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 is functional FinSequence-membered V89() set
(dom a) /\ ((arity a) -tuples_on L) is set
(arity a) -tuples_on the carrier of U0 is non empty functional FinSequence-membered FinSequenceSet of the carrier of U0
((arity a) -tuples_on the carrier of U0) /\ ((arity a) -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)
a * is non empty functional FinSequence-membered FinSequenceSet of 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)
a * is non empty functional FinSequence-membered FinSequenceSet of 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)
a * is non empty functional FinSequence-membered FinSequenceSet of 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)
y * is non empty functional FinSequence-membered FinSequenceSet of 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
(arity b) -tuples_on y is non empty functional FinSequence-membered FinSequenceSet of y
b | ((arity 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 a is functional FinSequence-membered V89() set
dom b is functional FinSequence-membered V89() set
(dom b) /\ ((arity b) -tuples_on y) is set
(arity b) -tuples_on the carrier of L is non empty functional FinSequence-membered FinSequenceSet of the carrier of L
((arity b) -tuples_on the carrier of L) /\ ((arity b) -tuples_on y) is set
(arity a) -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)
a * is non empty functional FinSequence-membered FinSequenceSet of 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)
L * is non empty functional FinSequence-membered FinSequenceSet of 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)
b * is non empty functional FinSequence-membered FinSequenceSet of 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)
x * is non empty functional FinSequence-membered FinSequenceSet of 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)
y * is non empty functional FinSequence-membered FinSequenceSet of 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)
dom u23 is functional FinSequence-membered V89() set
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)
dom u12 is functional FinSequence-membered V89() set
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
dom y is functional FinSequence-membered V89() set
arity y is V29() V30() V31() V35() V36() V41() Element of NAT
(arity y) -tuples_on the carrier of a is non empty functional FinSequence-membered FinSequenceSet of the carrier of a
(arity y) -tuples_on b is non empty functional FinSequence-membered FinSequenceSet of b
y | ((arity 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 | ((arity y) -tuples_on b)) is functional FinSequence-membered set
(dom y) /\ ((arity 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
C is Relation-like NAT -defined x -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of x
rng u12 is set
rng C is set
len C is V29() V30() V31() V35() V36() V41() Element of NAT
o1 is Relation-like NAT -defined b -valued Function-like V36() FinSequence-like FinSubsequence-like Element of b *
{ b1 where b1 is Relation-like NAT -defined b -valued Function-like V36() FinSequence-like FinSubsequence-like Element of b * : len b1 = arity y } is set
o0 is Relation-like NAT -defined the carrier of U0 -valued Function-like V36() FinSequence-like FinSubsequence-like Element of the carrier of U0 *
{ 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
B is Relation-like NAT -defined y -valued Function-like V36() FinSequence-like FinSubsequence-like Element of y *
{ b1 where b1 is Relation-like NAT -defined y -valued Function-like V36() FinSequence-like FinSubsequence-like Element of y * : len b1 = arity u23 } is set
(u23 | ((arity u23) -tuples_on y)) . B is set
u23 . B is set
(y | ((arity 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
(arity z) -tuples_on x is non empty functional FinSequence-membered FinSequenceSet of x
z | ((arity 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:]
(arity z) -tuples_on b is non empty functional FinSequence-membered FinSequenceSet of b
((arity z) -tuples_on b) /\ ((arity z) -tuples_on x) is set
z | (((arity z) -tuples_on b) /\ ((arity 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:]
z | ((arity 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 | ((arity z) -tuples_on b)) | ((arity 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:]
(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) | ((arity z) -tuples_on x) is Relation-like b * -defined b -valued Function-like Element of bool [:(b *),b:]
u23 | ((arity z) -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)
b * is non empty functional FinSequence-membered FinSequenceSet of 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)
x * is non empty functional FinSequence-membered FinSequenceSet of 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)
y * is non empty functional FinSequence-membered FinSequenceSet of 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)
z is Relation-like NAT -defined x -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of x
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
b * is non empty functional FinSequence-membered FinSequenceSet of b
(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
{ b1 where b1 is Relation-like NAT -defined y -valued Function-like V36() FinSequence-like FinSubsequence-like Element of y * : len b1 = arity u12 } is set
C is Relation-like NAT -defined y -valued Function-like V36() FinSequence-like FinSubsequence-like Element of y *
B is Relation-like NAT -defined b -valued Function-like V36() FinSequence-like FinSubsequence-like Element of b *
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)
b * is non empty functional FinSequence-membered FinSequenceSet of 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
(arity z) -tuples_on b is non empty functional FinSequence-membered FinSequenceSet of b
z | ((arity 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
(arity z) -tuples_on y is non empty functional FinSequence-membered FinSequenceSet of y
((arity z) -tuples_on y) /\ ((arity z) -tuples_on b) is set
z | (((arity z) -tuples_on y) /\ ((arity 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:]
z | ((arity 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:]
(arity z) -tuples_on x is non empty functional FinSequence-membered FinSequenceSet of x
(z | ((arity z) -tuples_on y)) | ((arity z) -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) | ((arity 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
signature U0 is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of NAT
signature L is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of NAT
dom (signature U0) is Element of bool NAT
len (signature U0) 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 (signature L) 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 (signature L) 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)
y * is non empty functional FinSequence-membered FinSequenceSet of 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
(signature U0) . y is set
(signature L) . 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)
L * is non empty functional FinSequence-membered FinSequenceSet of 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)
L * is non empty functional FinSequence-membered FinSequenceSet of 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)
b * is non empty functional FinSequence-membered FinSequenceSet of 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)
b * is non empty functional FinSequence-membered FinSequenceSet of 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
u23 is Relation-like NAT -defined b -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of b
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
u12 is Relation-like NAT -defined the carrier of a -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of the carrier of a
y . u12 is set
B is non empty Element of bool the carrier of U0
C is Relation-like NAT -defined the carrier of L -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of the carrier of L
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)
y * is non empty functional FinSequence-membered FinSequenceSet of 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)
z * is non empty functional FinSequence-membered FinSequenceSet of 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)
b * is non empty functional FinSequence-membered FinSequenceSet of 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
dom <*a*> is Element of bool NAT
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)
dom y is functional FinSequence-membered V89() set
y is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like set
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
dom L is functional FinSequence-membered V89() 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
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
dom y is functional FinSequence-membered V89() 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
<*> b is empty proper Relation-like NAT -defined b -valued Function-like functional V29() V30() V31() V33() V34() V35() V36() V41() V43( {} ) FinSequence-like FinSubsequence-like FinSequence-membered V89() FinSequence of b
[:NAT,b:] is non empty V36() set
{(<*> b)} is non empty trivial V43(1) set
0 -tuples_on b is non empty functional FinSequence-membered FinSequenceSet of b
(arity y) -tuples_on b is non empty functional FinSequence-membered FinSequenceSet of b
(dom y) /\ ((arity y) -tuples_on b) is set
y | ((arity 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 | ((arity 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)
b * is non empty functional FinSequence-membered FinSequenceSet of 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 | ((arity 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 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
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 U0 is non empty set
(U0) is non empty Element of bool the carrier of U0
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
the Element of (U0) is Element of (U0)
bool the carrier of L is non empty set
bool the carrier of a is non empty set
the carrier of L /\ the carrier of a 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 Element of bool the carrier of U0
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 Element of bool the carrier of U0
bool the carrier of U0 is non empty Element of bool (bool the carrier of U0)
bool (bool the carrier of U0) is non empty set
b is set
meet b is set
y is non empty Element of bool the carrier of U0
y is set
y is set
L \/ (U0) is Element of bool the carrier of U0
y is non empty Element of bool the carrier of U0
(U0,y) is non empty strict V84() quasi_total non-empty (U0)
y is non empty strict V84() quasi_total non-empty (U0)
the carrier of y is non empty 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)
u23 is Relation-like NAT -defined y -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of y
len u23 is V29() V30() V31() V35() V36() V41() Element of NAT
arity z is V29() V30() V31() V35() V36() V41() Element of NAT
z . u23 is set
rng u23 is set
u12 is set
C is Element of bool the carrier of U0
B is non empty Element of bool the carrier of U0
o0 is Relation-like NAT -defined B -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of B
z . o0 is set
(U0,y) is Relation-like NAT -defined PFuncs ((y *),y) -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of PFuncs ((y *),y)
y * is non empty functional FinSequence-membered FinSequenceSet of y
PFuncs ((y *),y) is non empty functional set
UAStr(# y,(U0,y) #) is non empty strict UAStr
z is non empty V84() quasi_total non-empty (U0)
the carrier of z is non empty set
C is set
B is Element of the carrier of U0
o0 is non empty Relation-like the carrier of U0 * -defined the carrier of U0 -valued Function-like homogeneous quasi_total Element of (U0)
arity o0 is V29() V30() V31() V35() V36() V41() Element of NAT
rng o0 is set
o0 is non empty Relation-like the carrier of U0 * -defined the carrier of U0 -valued Function-like homogeneous quasi_total Element of (U0)
arity o0 is V29() V30() V31() V35() V36() V41() Element of NAT
rng o0 is set
dom o0 is functional FinSequence-membered V89() set
o1 is set
o0 . o1 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
u12 is non empty Element of bool the carrier of U0
<*> u12 is empty proper Relation-like NAT -defined u12 -valued Function-like functional V29() V30() V31() V33() V34() V35() V36() V41() V43( {} ) FinSequence-like FinSubsequence-like FinSequence-membered V89() FinSequence of u12
[:NAT,u12:] is non empty V36() set
{(<*> u12)} is non empty trivial V43(1) set
0 -tuples_on u12 is non empty functional FinSequence-membered FinSequenceSet of u12
(arity o0) -tuples_on u12 is non empty functional FinSequence-membered FinSequenceSet of u12
(dom o0) /\ ((arity o0) -tuples_on u12) is set
o0 | ((arity o0) -tuples_on u12) 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 (o0 | ((arity o0) -tuples_on u12)) is functional FinSequence-membered set
dom the charact of U0 is Element of bool NAT
s is V29() V30() V31() V35() V36() V41() set
the charact of U0 . s is homogeneous set
the charact of z is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of z *), the carrier of z) -valued Function-like Function-yielding V36() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of z *), the carrier of z)
the carrier of z * is non empty functional FinSequence-membered FinSequenceSet of the carrier of z
PFuncs (( the carrier of z *), the carrier of z) is non empty functional set
dom the charact of z is Element of bool NAT
(z) is non empty PFuncsDomHQN of the carrier of z
rng the charact of z is set
the charact of z . s is homogeneous set
(U0,u12) is Relation-like NAT -defined PFuncs ((u12 *),u12) -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of PFuncs ((u12 *),u12)
u12 * is non empty functional FinSequence-membered FinSequenceSet of u12
PFuncs ((u12 *),u12) is non empty functional set
sE is non empty Relation-like the carrier of z * -defined the carrier of z -valued Function-like homogeneous quasi_total Element of (z)
(U0,u12,o0) is non empty Relation-like u12 * -defined u12 -valued Function-like homogeneous quasi_total Element of bool [:(u12 *),u12:]
[:(u12 *),u12:] is non empty set
bool [:(u12 *),u12:] is non empty set
dom (U0,u12,o0) is functional FinSequence-membered V89() set
sE . o1 is set
rng sE is set
(o0 | ((arity o0) -tuples_on u12)) . o1 is set
u12 is non empty Element of bool the carrier of U0
bool the carrier of z 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
u12 is non empty Element of bool the carrier of z
(z,u12) is Relation-like NAT -defined PFuncs ((u12 *),u12) -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of PFuncs ((u12 *),u12)
u12 * is non empty functional FinSequence-membered FinSequenceSet of u12
PFuncs ((u12 *),u12) is non empty functional set
the charact of z is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of z *), the carrier of z) -valued Function-like Function-yielding V36() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of z *), the carrier of z)
the carrier of z * is non empty functional FinSequence-membered FinSequenceSet of the carrier of z
PFuncs (( the carrier of z *), the carrier of z) is non empty functional set
C is non empty Element of bool the carrier of U0
(U0,C) is Relation-like NAT -defined PFuncs ((C *),C) -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of PFuncs ((C *),C)
C * is non empty functional FinSequence-membered FinSequenceSet of C
PFuncs ((C *),C) is non empty functional set
dom the charact of U0 is Element of bool NAT
dom (U0,C) is Element of bool NAT
(z) is non empty PFuncsDomHQN of the carrier of z
rng the charact of z is set
dom the charact of z is Element of bool NAT
B is non empty Relation-like the carrier of z * -defined the carrier of z -valued Function-like homogeneous quasi_total Element of (z)
o0 is V29() V30() V31() V35() V36() V41() set
the charact of z . o0 is homogeneous set
the charact of U0 . o0 is homogeneous set
o1 is non empty Relation-like the carrier of U0 * -defined the carrier of U0 -valued Function-like homogeneous quasi_total Element of (U0)
arity o1 is V29() V30() V31() V35() V36() V41() Element of NAT
arity B is V29() V30() V31() V35() V36() V41() Element of NAT
s is Relation-like NAT -defined u12 -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of u12
(arity o1) -tuples_on C is non empty functional FinSequence-membered FinSequenceSet of C
o1 | ((arity o1) -tuples_on C) 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 (o1 | ((arity o1) -tuples_on C)) is functional FinSequence-membered set
dom o1 is functional FinSequence-membered V89() set
(dom o1) /\ ((arity o1) -tuples_on C) is set
(arity o1) -tuples_on the carrier of U0 is non empty functional FinSequence-membered FinSequenceSet of the carrier of U0
((arity o1) -tuples_on the carrier of U0) /\ ((arity o1) -tuples_on C) is set
len s is V29() V30() V31() V35() V36() V41() Element of NAT
s1 is Relation-like NAT -defined C -valued Function-like V36() FinSequence-like FinSubsequence-like Element of C *
{ b1 where b1 is Relation-like NAT -defined C -valued Function-like V36() FinSequence-like FinSubsequence-like Element of C * : len b1 = arity o1 } is set
B . s is set
(U0,C,o1) is non empty Relation-like C * -defined C -valued Function-like homogeneous quasi_total Element of bool [:(C *),C:]
[:(C *),C:] is non empty set
bool [:(C *),C:] is non empty set
(U0,C,o1) . s1 is set
(o1 | ((arity o1) -tuples_on C)) . s1 is set
sE is Relation-like NAT -defined y -valued Function-like V36() FinSequence-like FinSubsequence-like Element of y *
o1 . sE is set
dom (z,u12) is Element of bool NAT
dom (U0,y) is Element of bool NAT
B is V29() V30() V31() V35() V36() V41() set
the charact of U0 . B is homogeneous set
the charact of z . B is homogeneous set
o0 is non empty Relation-like the carrier of U0 * -defined the carrier of U0 -valued Function-like homogeneous quasi_total Element of (U0)
the charact of y . B is homogeneous set
(U0,y,o0) 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 o0 is V29() V30() V31() V35() V36() V41() Element of NAT
(arity o0) -tuples_on y is non empty functional FinSequence-membered FinSequenceSet of y
o0 | ((arity o0) -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:]
(arity o0) -tuples_on C is non empty functional FinSequence-membered FinSequenceSet of C
((arity o0) -tuples_on C) /\ ((arity o0) -tuples_on y) is set
o0 | (((arity o0) -tuples_on C) /\ ((arity o0) -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:]
o0 | ((arity o0) -tuples_on C) 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:]
(o0 | ((arity o0) -tuples_on C)) | ((arity o0) -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:]
(U0,C,o0) is non empty Relation-like C * -defined C -valued Function-like homogeneous quasi_total Element of bool [:(C *),C:]
(U0,C,o0) | ((arity o0) -tuples_on y) is Relation-like C * -defined C -valued Function-like Element of bool [:(C *),C:]
o1 is non empty Relation-like the carrier of z * -defined the carrier of z -valued Function-like homogeneous quasi_total Element of (z)
o1 | ((arity o0) -tuples_on y) is Relation-like the carrier of z * -defined the carrier of z -valued Function-like Element of bool [:( the carrier of z *), the carrier of z:]
[:( the carrier of z *), the carrier of z:] is non empty set
bool [:( the carrier of z *), the carrier of z:] is non empty set
arity o1 is V29() V30() V31() V35() V36() V41() Element of NAT
(arity o1) -tuples_on u12 is non empty functional FinSequence-membered FinSequenceSet of u12
o1 | ((arity o1) -tuples_on u12) is Relation-like the carrier of z * -defined the carrier of z -valued Function-like Element of bool [:( the carrier of z *), the carrier of z:]
(z,u12,o1) is non empty Relation-like u12 * -defined u12 -valued Function-like homogeneous quasi_total Element of bool [:(u12 *),u12:]
[:(u12 *),u12:] is non empty set
bool [:(u12 *),u12:] is non empty set
(z,u12) . B is set
a is non empty strict V84() quasi_total non-empty (U0)
the carrier of a is non empty set
b is non empty strict V84() quasi_total non-empty (U0)
the carrier of b is non empty set
U0 is non empty strict V84() quasi_total non-empty UAStr
the carrier of U0 is non empty set
[#] the carrier of U0 is non empty non proper Element of bool the carrier of U0
bool the carrier of U0 is non empty set
(U0,([#] the carrier of U0)) is non empty strict V84() quasi_total non-empty (U0)
the carrier of (U0,([#] 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
dom the charact of U0 is Element of bool NAT
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)
a * is non empty functional FinSequence-membered FinSequenceSet of a
PFuncs ((a *),a) is non empty functional set
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
the charact of (U0,([#] the carrier of U0)) is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of (U0,([#] the carrier of U0)) *), 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,([#] the carrier of U0)))
the carrier of (U0,([#] the carrier of U0)) * is non empty functional FinSequence-membered FinSequenceSet of the carrier of (U0,([#] the carrier of U0))
PFuncs (( the carrier of (U0,([#] the carrier of U0)) *), the carrier of (U0,([#] the carrier of U0))) 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
L is non empty strict V84() quasi_total non-empty (U0)
the carrier of L is non empty set
a is non empty Element of bool the carrier of U0
(U0,a) is non empty strict V84() quasi_total non-empty (U0)
the carrier of (U0,a) is non empty set
bool the carrier of 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 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 non empty set
b is non empty set
x is non empty Element of bool the carrier of U0
(U0,x) is non empty strict V84() quasi_total non-empty (U0)
y is non empty Element of bool the carrier of U0
(U0,y) is non empty strict V84() quasi_total non-empty (U0)
x is non empty strict V84() quasi_total non-empty (U0)
y is non empty strict V84() quasi_total non-empty (U0)
b is non empty set
y is non empty Element of bool the carrier of U0
(U0,y) is non empty strict V84() quasi_total non-empty (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
(U0) is Element of bool the carrier of U0
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
a is Element of bool the carrier of U0
b is Element of bool the carrier of U0
a \/ the carrier of L is non empty set
(U0,a) is non empty strict V84() quasi_total non-empty (U0)
(U0,(U0,a),L) is non empty strict V84() quasi_total non-empty (U0)
(U0,b) is non empty strict V84() quasi_total non-empty (U0)
the carrier of (U0,a) is non empty set
the carrier of (U0,b) is non empty set
the carrier of (U0,a) /\ the carrier of (U0,b) is set
bool the carrier of (U0,a) is non empty set
bool the carrier of (U0,b) is non empty set
the carrier of (U0,a) /\ the carrier of (U0,b) is set
the carrier of (U0,a) /\ the carrier of (U0,b) is set
the carrier of (U0,a) /\ the carrier of (U0,b) is set
(U0,(U0,a),(U0,b)) is non empty strict V84() quasi_total non-empty (U0)
the carrier of (U0,(U0,a),(U0,b)) is non empty set
y is non empty Element of bool the carrier of U0
x is non empty Element of bool the carrier of U0
y \/ x is non empty Element of bool the carrier of U0
bool the carrier of (U0,(U0,a),(U0,b)) is non empty set
y is non empty Element of bool the carrier of U0
(U0,y) is non empty strict V84() quasi_total non-empty (U0)
the carrier of (U0,(U0,a),L) is non empty set
a \/ x is non empty Element of bool the carrier of U0
U0 is non empty V84() quasi_total non-empty UAStr
L is non empty V84() quasi_total non-empty (U0)
a is non empty V84() quasi_total non-empty (U0)
(U0,L,a) is non empty strict V84() quasi_total non-empty (U0)
(U0,a,L) is non empty strict V84() quasi_total non-empty (U0)
the carrier of U0 is non empty set
bool the carrier of U0 is non empty set
the carrier of L is non empty set
the carrier of a is non empty set
b is non empty Element of bool the carrier of U0
x is non empty Element of bool the carrier of U0
b \/ x is non empty Element of bool the carrier of U0
y is non empty Element of bool the carrier of U0
(U0,y) is non empty strict V84() quasi_total non-empty (U0)
U0 is non empty V84() quasi_total non-empty () UAStr
L is non empty strict V84() quasi_total non-empty (U0)
a is non empty strict V84() quasi_total non-empty (U0)
(U0,L,a) is non empty strict V84() quasi_total non-empty (U0)
(U0,L,(U0,L,a)) is non empty strict V84() quasi_total non-empty (U0)
the carrier of U0 is non empty set
bool the carrier of U0 is non empty set
the carrier of (U0,L,(U0,L,a)) is non empty set
the carrier of L is non empty set
the carrier of a is non empty set
x is non empty Element of bool the carrier of U0
y is non empty Element of bool the carrier of U0
x \/ y is non empty Element of bool the carrier of U0
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
(U0,x) is Relation-like NAT -defined PFuncs ((x *),x) -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of PFuncs ((x *),x)
x * is non empty functional FinSequence-membered FinSequenceSet of x
PFuncs ((x *),x) is non empty functional set
dom (U0,x) 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
y is non empty Element of bool the carrier of U0
(U0,y) is non empty strict V84() quasi_total non-empty (U0)
the carrier of (U0,L,a) is non empty set
the carrier of L /\ the carrier of (U0,L,a) is 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)
b * is non empty functional FinSequence-membered FinSequenceSet of b
PFuncs ((b *),b) is non empty functional set
dom (U0,b) is Element of bool NAT
the charact of (U0,L,(U0,L,a)) is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of (U0,L,(U0,L,a)) *), the carrier of (U0,L,(U0,L,a))) -valued Function-like Function-yielding V36() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of (U0,L,(U0,L,a)) *), the carrier of (U0,L,(U0,L,a)))
the carrier of (U0,L,(U0,L,a)) * is non empty functional FinSequence-membered FinSequenceSet of the carrier of (U0,L,(U0,L,a))
PFuncs (( the carrier of (U0,L,(U0,L,a)) *), the carrier of (U0,L,(U0,L,a))) is non empty functional set
z is V29() V30() V31() V35() V36() V41() set
the charact of (U0,L,(U0,L,a)) . z is homogeneous set
the charact of L . z is homogeneous set
(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
(U0,b) . z is set
u23 is non empty Relation-like the carrier of U0 * -defined the carrier of U0 -valued Function-like homogeneous quasi_total Element of (U0)
(U0,b,u23) 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
(U0,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
(U0,x) . z is set
U0 is non empty V84() quasi_total non-empty () UAStr
L is non empty strict V84() quasi_total non-empty (U0)
a is non empty strict V84() quasi_total non-empty (U0)
(U0,L,a) is non empty strict V84() quasi_total non-empty (U0)
(U0,(U0,L,a),a) is non empty strict V84() quasi_total non-empty (U0)
the carrier of U0 is non empty set
bool the carrier of U0 is non empty set
the carrier of (U0,L,a) is non empty set
the carrier of a is non empty set
b is non empty Element of bool the carrier of U0
x is non empty Element of bool the carrier of U0
b \/ x is non empty Element of bool the carrier of U0
the carrier of L is non empty set
the carrier of L /\ the carrier of a is set
y is non empty Element of bool the carrier of U0
(U0,y) is non empty strict V84() quasi_total non-empty (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
{ (U0,b1) where b1 is Element of bool the carrier of U0 : not b1 is empty } is set
L is set
a is set
b is Element of bool the carrier of U0
(U0,b) is non empty strict V84() quasi_total non-empty (U0)
b is non empty strict V84() quasi_total non-empty (U0)
the carrier of b is non empty set
x is non empty Element of bool the carrier of U0
(U0,x) is non empty strict V84() quasi_total non-empty (U0)
L is set
a is set
b is set
b is set
U0 is non empty V84() quasi_total non-empty UAStr
(U0) is set
the non empty strict V84() quasi_total non-empty (U0) is non empty strict V84() quasi_total non-empty (U0)
U0 is non empty V84() quasi_total non-empty UAStr
(U0) is non empty set
[:(U0),(U0):] is non empty set
[:[:(U0),(U0):],(U0):] is non empty set
bool [:[:(U0),(U0):],(U0):] is non empty set
L is Element of (U0)
a is Element of (U0)
b is non empty strict V84() quasi_total non-empty (U0)
x is non empty strict V84() quasi_total non-empty (U0)
(U0,b,x) is non empty strict V84() quasi_total non-empty (U0)
y is Element of (U0)
y is non empty strict V84() quasi_total non-empty (U0)
z is non empty strict V84() quasi_total non-empty (U0)
(U0,y,z) is non empty strict V84() quasi_total non-empty (U0)
L is Relation-like [:(U0),(U0):] -defined (U0) -valued Function-like V21([:(U0),(U0):],(U0)) Element of bool [:[:(U0),(U0):],(U0):]
a is Element of (U0)
x is non empty strict V84() quasi_total non-empty (U0)
b is Element of (U0)
y is non empty strict V84() quasi_total non-empty (U0)
L . (a,b) is Element of (U0)
(U0,x,y) is non empty strict V84() quasi_total non-empty (U0)
L is Relation-like [:(U0),(U0):] -defined (U0) -valued Function-like V21([:(U0),(U0):],(U0)) Element of bool [:[:(U0),(U0):],(U0):]
a is Relation-like [:(U0),(U0):] -defined (U0) -valued Function-like V21([:(U0),(U0):],(U0)) Element of bool [:[:(U0),(U0):],(U0):]
b is Element of (U0)
x is Element of (U0)
L . (b,x) is Element of (U0)
a . (b,x) is Element of (U0)
y is non empty strict V84() quasi_total non-empty (U0)
y is non empty strict V84() quasi_total non-empty (U0)
(U0,y,y) is non empty strict V84() quasi_total non-empty (U0)
U0 is non empty V84() quasi_total non-empty UAStr
(U0) is non empty set
[:(U0),(U0):] is non empty set
[:[:(U0),(U0):],(U0):] is non empty set
bool [:[:(U0),(U0):],(U0):] is non empty set
L is Element of (U0)
a is Element of (U0)
b is non empty strict V84() quasi_total non-empty (U0)
x is non empty strict V84() quasi_total non-empty (U0)
(U0,b,x) is non empty strict V84() quasi_total non-empty (U0)
y is Element of (U0)
y is non empty strict V84() quasi_total non-empty (U0)
z is non empty strict V84() quasi_total non-empty (U0)
(U0,y,z) is non empty strict V84() quasi_total non-empty (U0)
L is Relation-like [:(U0),(U0):] -defined (U0) -valued Function-like V21([:(U0),(U0):],(U0)) Element of bool [:[:(U0),(U0):],(U0):]
a is Element of (U0)
x is non empty strict V84() quasi_total non-empty (U0)
b is Element of (U0)
y is non empty strict V84() quasi_total non-empty (U0)
L . (a,b) is Element of (U0)
(U0,x,y) is non empty strict V84() quasi_total non-empty (U0)
L is Relation-like [:(U0),(U0):] -defined (U0) -valued Function-like V21([:(U0),(U0):],(U0)) Element of bool [:[:(U0),(U0):],(U0):]
a is Relation-like [:(U0),(U0):] -defined (U0) -valued Function-like V21([:(U0),(U0):],(U0)) Element of bool [:[:(U0),(U0):],(U0):]
b is Element of (U0)
x is Element of (U0)
L . (b,x) is Element of (U0)
a . (b,x) is Element of (U0)
y is non empty strict V84() quasi_total non-empty (U0)
y is non empty strict V84() quasi_total non-empty (U0)
(U0,y,y) is non empty strict V84() quasi_total non-empty (U0)
U0 is non empty V84() quasi_total non-empty UAStr
(U0) is non empty set
(U0) is Relation-like [:(U0),(U0):] -defined (U0) -valued Function-like V21([:(U0),(U0):],(U0)) Element of bool [:[:(U0),(U0):],(U0):]
[:(U0),(U0):] is non empty set
[:[:(U0),(U0):],(U0):] is non empty set
bool [:[:(U0),(U0):],(U0):] is non empty set
a is Element of (U0)
b is Element of (U0)
(U0) . (a,b) is Element of (U0)
(U0) . (b,a) is Element of (U0)
x is non empty strict V84() quasi_total non-empty (U0)
the carrier of x is non empty set
y is non empty strict V84() quasi_total non-empty (U0)
the carrier of y is non empty set
the carrier of x \/ the carrier of y is non empty set
the carrier of U0 is non empty set
bool the carrier of U0 is non empty set
y is non empty set
(U0,x,y) is non empty strict V84() quasi_total non-empty (U0)
z is non empty Element of bool the carrier of U0
(U0,z) is non empty strict V84() quasi_total non-empty (U0)
(U0,y,x) is non empty strict V84() quasi_total non-empty (U0)
U0 is non empty V84() quasi_total non-empty UAStr
(U0) is non empty set
(U0) is Relation-like [:(U0),(U0):] -defined (U0) -valued Function-like V21([:(U0),(U0):],(U0)) Element of bool [:[:(U0),(U0):],(U0):]
[:(U0),(U0):] is non empty set
[:[:(U0),(U0):],(U0):] is non empty set
bool [:[:(U0),(U0):],(U0):] is non empty set
a is Element of (U0)
b is Element of (U0)
x is Element of (U0)
(U0) . (b,x) is Element of (U0)
(U0) . (a,((U0) . (b,x))) is Element of (U0)
(U0) . (a,b) is Element of (U0)
(U0) . (((U0) . (a,b)),x) is Element of (U0)
y is non empty strict V84() quasi_total non-empty (U0)
the carrier of y is non empty set
y is non empty strict V84() quasi_total non-empty (U0)
the carrier of y is non empty set
z is non empty strict V84() quasi_total non-empty (U0)
the carrier of z is non empty set
the carrier of y \/ the carrier of z is non empty set
the carrier of y \/ ( the carrier of y \/ the carrier of z) is non empty set
(U0,y,y) is non empty strict V84() quasi_total non-empty (U0)
the carrier of U0 is non empty set
bool the carrier of U0 is non empty set
the carrier of y \/ the carrier of y is non empty set
u23 is non empty set
B is non empty Element of bool the carrier of U0
C is non empty Element of bool the carrier of U0
C \/ the carrier of z is non empty set
(U0,(U0,y,y),z) is non empty strict V84() quasi_total non-empty (U0)
(U0,C) is non empty strict V84() quasi_total non-empty (U0)
(U0,(U0,C),z) is non empty strict V84() quasi_total non-empty (U0)
(U0,B) is non empty strict V84() quasi_total non-empty (U0)
(U0,y,z) is non empty strict V84() quasi_total non-empty (U0)
(U0,y,(U0,y,z)) is non empty strict V84() quasi_total non-empty (U0)
u12 is non empty Element of bool the carrier of U0
(U0,u12) is non empty strict V84() quasi_total non-empty (U0)
(U0,y,(U0,u12)) is non empty strict V84() quasi_total non-empty (U0)
(U0,(U0,u12),y) is non empty strict V84() quasi_total non-empty (U0)
U0 is non empty V84() quasi_total non-empty () UAStr
(U0) is non empty set
(U0) is Relation-like [:(U0),(U0):] -defined (U0) -valued Function-like V21([:(U0),(U0):],(U0)) Element of bool [:[:(U0),(U0):],(U0):]
[:(U0),(U0):] is non empty set
[:[:(U0),(U0):],(U0):] is non empty set
bool [:[:(U0),(U0):],(U0):] is non empty set
a is Element of (U0)
b is Element of (U0)
(U0) . (a,b) is Element of (U0)
(U0) . (b,a) is Element of (U0)
x is non empty strict V84() quasi_total non-empty (U0)
y is non empty strict V84() quasi_total non-empty (U0)
(U0,x,y) is non empty strict V84() quasi_total non-empty (U0)
(U0,y,x) is non empty strict V84() quasi_total non-empty (U0)
the carrier of x is non empty set
the carrier of y is non empty set
the carrier of (U0,y,x) is non empty set
the carrier of y /\ the carrier of x is set
the carrier of U0 is non empty set
bool the carrier of U0 is non empty set
the charact of (U0,y,x) is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of (U0,y,x) *), the carrier of (U0,y,x)) -valued Function-like Function-yielding V36() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of (U0,y,x) *), the carrier of (U0,y,x))
the carrier of (U0,y,x) * is non empty functional FinSequence-membered FinSequenceSet of the carrier of (U0,y,x)
PFuncs (( the carrier of (U0,y,x) *), the carrier of (U0,y,x)) 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)
y * is non empty functional FinSequence-membered FinSequenceSet of y
PFuncs ((y *),y) is non empty functional set
U0 is non empty V84() quasi_total non-empty () UAStr
(U0) is non empty set
(U0) is Relation-like [:(U0),(U0):] -defined (U0) -valued Function-like V21([:(U0),(U0):],(U0)) Element of bool [:[:(U0),(U0):],(U0):]
[:(U0),(U0):] is non empty set
[:[:(U0),(U0):],(U0):] is non empty set
bool [:[:(U0),(U0):],(U0):] is non empty set
a is Element of (U0)
b is Element of (U0)
x is Element of (U0)
(U0) . (b,x) is Element of (U0)
(U0) . (a,((U0) . (b,x))) is Element of (U0)
(U0) . (a,b) is Element of (U0)
(U0) . (((U0) . (a,b)),x) is Element of (U0)
y is non empty strict V84() quasi_total non-empty (U0)
z is non empty strict V84() quasi_total non-empty (U0)
(U0,y,z) is non empty strict V84() quasi_total non-empty (U0)
y is non empty strict V84() quasi_total non-empty (U0)
(U0,y,y) is non empty strict V84() quasi_total non-empty (U0)
u23 is Element of (U0)
(U0) . (a,u23) is Element of (U0)
(U0,y,(U0,y,z)) is non empty strict V84() quasi_total non-empty (U0)
u12 is Element of (U0)
(U0) . (u12,x) is Element of (U0)
(U0,(U0,y,y),z) is non empty strict V84() quasi_total non-empty (U0)
the carrier of y is non empty set
the carrier of z is non empty set
the carrier of (U0,y,z) is non empty set
the carrier of y /\ the carrier of z is set
the carrier of y is non empty set
the carrier of U0 is non empty set
bool the carrier of U0 is non empty set
the carrier of (U0,y,(U0,y,z)) is non empty set
the charact of (U0,y,(U0,y,z)) is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of (U0,y,(U0,y,z)) *), the carrier of (U0,y,(U0,y,z))) -valued Function-like Function-yielding V36() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of (U0,y,(U0,y,z)) *), the carrier of (U0,y,(U0,y,z)))
the carrier of (U0,y,(U0,y,z)) * is non empty functional FinSequence-membered FinSequenceSet of the carrier of (U0,y,(U0,y,z))
PFuncs (( the carrier of (U0,y,(U0,y,z)) *), the carrier of (U0,y,(U0,y,z))) is non empty functional set
C is non empty Element of bool the carrier of U0
(U0,C) is Relation-like NAT -defined PFuncs ((C *),C) -valued Function-like V36() FinSequence-like FinSubsequence-like FinSequence of PFuncs ((C *),C)
C * is non empty functional FinSequence-membered FinSequenceSet of C
PFuncs ((C *),C) is non empty functional set
the carrier of y /\ ( the carrier of y /\ the carrier of z) is set
C is non empty Element of bool the carrier of U0
the carrier of y /\ the carrier of y is set
( the carrier of y /\ the carrier of y) /\ the carrier of z is set
the carrier of (U0,y,y) is non empty set
U0 is non empty V84() quasi_total non-empty () UAStr
(U0) is non empty set
(U0) is Relation-like [:(U0),(U0):] -defined (U0) -valued Function-like V21([:(U0),(U0):],(U0)) Element of bool [:[:(U0),(U0):],(U0):]
[:(U0),(U0):] is non empty set
[:[:(U0),(U0):],(U0):] is non empty set
bool [:[:(U0),(U0):],(U0):] is non empty set
(U0) is Relation-like [:(U0),(U0):] -defined (U0) -valued Function-like V21([:(U0),(U0):],(U0)) Element of bool [:[:(U0),(U0):],(U0):]
LattStr(# (U0),(U0),(U0) #) is non empty strict LattStr
the carrier of LattStr(# (U0),(U0),(U0) #) is non empty set
a is Element of the carrier of LattStr(# (U0),(U0),(U0) #)
b is Element of the carrier of LattStr(# (U0),(U0),(U0) #)
x is Element of the carrier of LattStr(# (U0),(U0),(U0) #)
b "\/" x is Element of the carrier of LattStr(# (U0),(U0),(U0) #)
a "\/" (b "\/" x) is Element of the carrier of LattStr(# (U0),(U0),(U0) #)
a "\/" b is Element of the carrier of LattStr(# (U0),(U0),(U0) #)
(a "\/" b) "\/" x is Element of the carrier of LattStr(# (U0),(U0),(U0) #)
the L_join of LattStr(# (U0),(U0),(U0) #) is Relation-like [: the carrier of LattStr(# (U0),(U0),(U0) #), the carrier of LattStr(# (U0),(U0),(U0) #):] -defined the carrier of LattStr(# (U0),(U0),(U0) #) -valued Function-like V21([: the carrier of LattStr(# (U0),(U0),(U0) #), the carrier of LattStr(# (U0),(U0),(U0) #):], the carrier of LattStr(# (U0),(U0),(U0) #)) Element of bool [:[: the carrier of LattStr(# (U0),(U0),(U0) #), the carrier of LattStr(# (U0),(U0),(U0) #):], the carrier of LattStr(# (U0),(U0),(U0) #):]
[: the carrier of LattStr(# (U0),(U0),(U0) #), the carrier of LattStr(# (U0),(U0),(U0) #):] is non empty set
[:[: the carrier of LattStr(# (U0),(U0),(U0) #), the carrier of LattStr(# (U0),(U0),(U0) #):], the carrier of LattStr(# (U0),(U0),(U0) #):] is non empty set
bool [:[: the carrier of LattStr(# (U0),(U0),(U0) #), the carrier of LattStr(# (U0),(U0),(U0) #):], the carrier of LattStr(# (U0),(U0),(U0) #):] is non empty set
the L_join of LattStr(# (U0),(U0),(U0) #) . (a,(b "\/" x)) is Element of the carrier of LattStr(# (U0),(U0),(U0) #)
y is Element of (U0)
y is Element of (U0)
z is Element of (U0)
(U0) . (y,z) is Element of (U0)
(U0) . (y,((U0) . (y,z))) is Element of (U0)
the L_join of LattStr(# (U0),(U0),(U0) #) . (a,b) is Element of the carrier of LattStr(# (U0),(U0),(U0) #)
the L_join of LattStr(# (U0),(U0),(U0) #) . (( the L_join of LattStr(# (U0),(U0),(U0) #) . (a,b)),x) is Element of the carrier of LattStr(# (U0),(U0),(U0) #)
( the L_join of LattStr(# (U0),(U0),(U0) #) . (a,b)) "\/" x is Element of the carrier of LattStr(# (U0),(U0),(U0) #)
a is Element of the carrier of LattStr(# (U0),(U0),(U0) #)
b is Element of the carrier of LattStr(# (U0),(U0),(U0) #)
a "/\" b is Element of the carrier of LattStr(# (U0),(U0),(U0) #)
b "/\" a is Element of the carrier of LattStr(# (U0),(U0),(U0) #)
x is Element of (U0)
y is Element of (U0)
(U0) . (x,y) is Element of (U0)
the L_meet of LattStr(# (U0),(U0),(U0) #) is Relation-like [: the carrier of LattStr(# (U0),(U0),(U0) #), the carrier of LattStr(# (U0),(U0),(U0) #):] -defined the carrier of LattStr(# (U0),(U0),(U0) #) -valued Function-like V21([: the carrier of LattStr(# (U0),(U0),(U0) #), the carrier of LattStr(# (U0),(U0),(U0) #):], the carrier of LattStr(# (U0),(U0),(U0) #)) Element of bool [:[: the carrier of LattStr(# (U0),(U0),(U0) #), the carrier of LattStr(# (U0),(U0),(U0) #):], the carrier of LattStr(# (U0),(U0),(U0) #):]
[: the carrier of LattStr(# (U0),(U0),(U0) #), the carrier of LattStr(# (U0),(U0),(U0) #):] is non empty set
[:[: the carrier of LattStr(# (U0),(U0),(U0) #), the carrier of LattStr(# (U0),(U0),(U0) #):], the carrier of LattStr(# (U0),(U0),(U0) #):] is non empty set
bool [:[: the carrier of LattStr(# (U0),(U0),(U0) #), the carrier of LattStr(# (U0),(U0),(U0) #):], the carrier of LattStr(# (U0),(U0),(U0) #):] is non empty set
the L_meet of LattStr(# (U0),(U0),(U0) #) . (b,a) is Element of the carrier of LattStr(# (U0),(U0),(U0) #)
a is Element of the carrier of LattStr(# (U0),(U0),(U0) #)
b is Element of the carrier of LattStr(# (U0),(U0),(U0) #)
a "\/" b is Element of the carrier of LattStr(# (U0),(U0),(U0) #)
a "/\" (a "\/" b) is Element of the carrier of LattStr(# (U0),(U0),(U0) #)
x is Element of (U0)
y is Element of (U0)
(U0) . (x,y) is Element of (U0)
(U0) . (x,((U0) . (x,y))) is Element of (U0)
y is non empty strict V84() quasi_total non-empty (U0)
z is non empty strict V84() quasi_total non-empty (U0)
(U0,y,z) is non empty strict V84() quasi_total non-empty (U0)
(U0,y,(U0,y,z)) is non empty strict V84() quasi_total non-empty (U0)
the L_meet of LattStr(# (U0),(U0),(U0) #) is Relation-like [: the carrier of LattStr(# (U0),(U0),(U0) #), the carrier of LattStr(# (U0),(U0),(U0) #):] -defined the carrier of LattStr(# (U0),(U0),(U0) #) -valued Function-like V21([: the carrier of LattStr(# (U0),(U0),(U0) #), the carrier of LattStr(# (U0),(U0),(U0) #):], the carrier of LattStr(# (U0),(U0),(U0) #)) Element of bool [:[: the carrier of LattStr(# (U0),(U0),(U0) #), the carrier of LattStr(# (U0),(U0),(U0) #):], the carrier of LattStr(# (U0),(U0),(U0) #):]
[: the carrier of LattStr(# (U0),(U0),(U0) #), the carrier of LattStr(# (U0),(U0),(U0) #):] is non empty set
[:[: the carrier of LattStr(# (U0),(U0),(U0) #), the carrier of LattStr(# (U0),(U0),(U0) #):], the carrier of LattStr(# (U0),(U0),(U0) #):] is non empty set
bool [:[: the carrier of LattStr(# (U0),(U0),(U0) #), the carrier of LattStr(# (U0),(U0),(U0) #):], the carrier of LattStr(# (U0),(U0),(U0) #):] is non empty set
the L_meet of LattStr(# (U0),(U0),(U0) #) . (a,(a "\/" b)) is Element of the carrier of LattStr(# (U0),(U0),(U0) #)
a is Element of the carrier of LattStr(# (U0),(U0),(U0) #)
b is Element of the carrier of LattStr(# (U0),(U0),(U0) #)
a "/\" b is Element of the carrier of LattStr(# (U0),(U0),(U0) #)
(a "/\" b) "\/" b is Element of the carrier of LattStr(# (U0),(U0),(U0) #)
x is Element of (U0)
y is Element of (U0)
(U0) . (x,y) is Element of (U0)
(U0) . (((U0) . (x,y)),y) is Element of (U0)
y is non empty strict V84() quasi_total non-empty (U0)
z is non empty strict V84() quasi_total non-empty (U0)
(U0,y,z) is non empty strict V84() quasi_total non-empty (U0)
(U0,(U0,y,z),z) is non empty strict V84() quasi_total non-empty (U0)
the L_join of LattStr(# (U0),(U0),(U0) #) is Relation-like [: the carrier of LattStr(# (U0),(U0),(U0) #), the carrier of LattStr(# (U0),(U0),(U0) #):] -defined the carrier of LattStr(# (U0),(U0),(U0) #) -valued Function-like V21([: the carrier of LattStr(# (U0),(U0),(U0) #), the carrier of LattStr(# (U0),(U0),(U0) #):], the carrier of LattStr(# (U0),(U0),(U0) #)) Element of bool [:[: the carrier of LattStr(# (U0),(U0),(U0) #), the carrier of LattStr(# (U0),(U0),(U0) #):], the carrier of LattStr(# (U0),(U0),(U0) #):]
[: the carrier of LattStr(# (U0),(U0),(U0) #), the carrier of LattStr(# (U0),(U0),(U0) #):] is non empty set
[:[: the carrier of LattStr(# (U0),(U0),(U0) #), the carrier of LattStr(# (U0),(U0),(U0) #):], the carrier of LattStr(# (U0),(U0),(U0) #):] is non empty set
bool [:[: the carrier of LattStr(# (U0),(U0),(U0) #), the carrier of LattStr(# (U0),(U0),(U0) #):], the carrier of LattStr(# (U0),(U0),(U0) #):] is non empty set
the L_join of LattStr(# (U0),(U0),(U0) #) . ((a "/\" b),b) is Element of the carrier of LattStr(# (U0),(U0),(U0) #)
a is Element of the carrier of LattStr(# (U0),(U0),(U0) #)
b is Element of the carrier of LattStr(# (U0),(U0),(U0) #)
x is Element of the carrier of LattStr(# (U0),(U0),(U0) #)
b "/\" x is Element of the carrier of LattStr(# (U0),(U0),(U0) #)
a "/\" (b "/\" x) is Element of the carrier of LattStr(# (U0),(U0),(U0) #)
a "/\" b is Element of the carrier of LattStr(# (U0),(U0),(U0) #)
(a "/\" b) "/\" x is Element of the carrier of LattStr(# (U0),(U0),(U0) #)
the L_meet of LattStr(# (U0),(U0),(U0) #) is Relation-like [: the carrier of LattStr(# (U0),(U0),(U0) #), the carrier of LattStr(# (U0),(U0),(U0) #):] -defined the carrier of LattStr(# (U0),(U0),(U0) #) -valued Function-like V21([: the carrier of LattStr(# (U0),(U0),(U0) #), the carrier of LattStr(# (U0),(U0),(U0) #):], the carrier of LattStr(# (U0),(U0),(U0) #)) Element of bool [:[: the carrier of LattStr(# (U0),(U0),(U0) #), the carrier of LattStr(# (U0),(U0),(U0) #):], the carrier of LattStr(# (U0),(U0),(U0) #):]
[: the carrier of LattStr(# (U0),(U0),(U0) #), the carrier of LattStr(# (U0),(U0),(U0) #):] is non empty set
[:[: the carrier of LattStr(# (U0),(U0),(U0) #), the carrier of LattStr(# (U0),(U0),(U0) #):], the carrier of LattStr(# (U0),(U0),(U0) #):] is non empty set
bool [:[: the carrier of LattStr(# (U0),(U0),(U0) #), the carrier of LattStr(# (U0),(U0),(U0) #):], the carrier of LattStr(# (U0),(U0),(U0) #):] is non empty set
the L_meet of LattStr(# (U0),(U0),(U0) #) . (a,(b "/\" x)) is Element of the carrier of LattStr(# (U0),(U0),(U0) #)
y is Element of (U0)
y is Element of (U0)
z is Element of (U0)
(U0) . (y,z) is Element of (U0)
(U0) . (y,((U0) . (y,z))) is Element of (U0)
the L_meet of LattStr(# (U0),(U0),(U0) #) . (a,b) is Element of the carrier of LattStr(# (U0),(U0),(U0) #)
the L_meet of LattStr(# (U0),(U0),(U0) #) . (( the L_meet of LattStr(# (U0),(U0),(U0) #) . (a,b)),x) is Element of the carrier of LattStr(# (U0),(U0),(U0) #)
( the L_meet of LattStr(# (U0),(U0),(U0) #) . (a,b)) "/\" x is Element of the carrier of LattStr(# (U0),(U0),(U0) #)
a is Element of the carrier of LattStr(# (U0),(U0),(U0) #)
b is Element of the carrier of LattStr(# (U0),(U0),(U0) #)
a "\/" b is Element of the carrier of LattStr(# (U0),(U0),(U0) #)
b "\/" a is Element of the carrier of LattStr(# (U0),(U0),(U0) #)
x is Element of (U0)
y is Element of (U0)
(U0) . (x,y) is Element of (U0)
the L_join of LattStr(# (U0),(U0),(U0) #) is Relation-like [: the carrier of LattStr(# (U0),(U0),(U0) #), the carrier of LattStr(# (U0),(U0),(U0) #):] -defined the carrier of LattStr(# (U0),(U0),(U0) #) -valued Function-like V21([: the carrier of LattStr(# (U0),(U0),(U0) #), the carrier of LattStr(# (U0),(U0),(U0) #):], the carrier of LattStr(# (U0),(U0),(U0) #)) Element of bool [:[: the carrier of LattStr(# (U0),(U0),(U0) #), the carrier of LattStr(# (U0),(U0),(U0) #):], the carrier of LattStr(# (U0),(U0),(U0) #):]
[: the carrier of LattStr(# (U0),(U0),(U0) #), the carrier of LattStr(# (U0),(U0),(U0) #):] is non empty set
[:[: the carrier of LattStr(# (U0),(U0),(U0) #), the carrier of LattStr(# (U0),(U0),(U0) #):], the carrier of LattStr(# (U0),(U0),(U0) #):] is non empty set
bool [:[: the carrier of LattStr(# (U0),(U0),(U0) #), the carrier of LattStr(# (U0),(U0),(U0) #):], the carrier of LattStr(# (U0),(U0),(U0) #):] is non empty set
the L_join of LattStr(# (U0),(U0),(U0) #) . (b,a) is Element of the carrier of LattStr(# (U0),(U0),(U0) #)