REAL is non empty non trivial non finite non empty-membered set
NAT is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal non empty-membered countable denumerable Element of bool REAL
bool REAL is non empty non trivial non finite non empty-membered set
omega is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal non empty-membered countable denumerable set
bool omega is non empty non trivial non finite non empty-membered set
bool NAT is non empty non trivial non finite non empty-membered set
COMPLEX is non empty non trivial non finite non empty-membered set
RAT is non empty non trivial non finite non empty-membered set
INT is non empty non trivial non finite non empty-membered set
[:REAL,REAL:] is Relation-like non empty non trivial non finite non empty-membered set
bool [:REAL,REAL:] is non empty non trivial non finite non empty-membered set
K281() is non empty strict multMagma
the U1 of K281() is set
<REAL,+> is non empty strict V94() V95() associative commutative left-invertible right-invertible invertible left-cancelable right-cancelable V153() multMagma
K287() is non empty strict associative commutative left-cancelable right-cancelable V153() SubStr of <REAL,+>
<NAT,+> is non empty strict V94() associative commutative left-cancelable right-cancelable V153() uniquely-decomposable SubStr of K287()
<REAL,*> is non empty strict V94() associative commutative multMagma
<NAT,*> is non empty strict V94() associative commutative uniquely-decomposable SubStr of <REAL,*>
{} is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty trivial complex epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural real integer finite finite-yielding finite-membered cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative Function-yielding V159() FuncSeq-like Cardinal-yielding countable FinSequence-yielding finite-support set
the Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty trivial complex epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural real integer finite finite-yielding finite-membered cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative Function-yielding V159() FuncSeq-like Cardinal-yielding countable FinSequence-yielding finite-support set is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty trivial complex epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural real integer finite finite-yielding finite-membered cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative Function-yielding V159() FuncSeq-like Cardinal-yielding countable FinSequence-yielding finite-support set
2 is non empty complex epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal ext-real positive non negative countable Element of NAT
1 is non empty complex epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal ext-real positive non negative countable Element of NAT
{{},1} is non empty finite finite-membered countable set
K391(NAT) is V165() set
BOOLEAN is set
0 is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty trivial complex epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural real integer finite finite-yielding finite-membered cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative Function-yielding V159() FuncSeq-like Cardinal-yielding countable FinSequence-yielding finite-support Element of NAT
{0,1} is non empty finite finite-membered countable set
[:{},{}:] is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty trivial complex epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural real integer finite finite-yielding finite-membered cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative Function-yielding V159() FuncSeq-like Cardinal-yielding countable FinSequence-yielding finite-support set
3 is non empty complex epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal ext-real positive non negative countable Element of NAT
{{}} is functional non empty trivial finite finite-membered 1 -element with_common_domain countable set
[:{{}},omega:] is Relation-like non empty non trivial non finite non empty-membered set
omega \/ [:{{}},omega:] is non empty set
[{},{}] is non empty V15() set
{[{},{}]} is Relation-like Function-like constant non empty trivial finite 1 -element with_non-empty_elements non empty-membered countable finite-support set
(omega \/ [:{{}},omega:]) \ {[{},{}]} is Element of bool (omega \/ [:{{}},omega:])
bool (omega \/ [:{{}},omega:]) is non empty set
Seg 1 is non empty trivial finite 1 -element countable Element of bool NAT
{ b1 where b1 is complex epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal ext-real non negative countable Element of NAT : ( 1 <= b1 & b1 <= 1 ) } is set
{} * is functional non empty FinSequence-membered FinSequenceSet of {}
K587() is set
K588() is set
U is non empty set
[:U,U:] is Relation-like non empty set
[:[:U,U:],U:] is Relation-like non empty set
bool [:[:U,U:],U:] is non empty set
U is set
pr1 (U,U) is Relation-like [:U,U:] -defined U -valued Function-like quasi_total Element of bool [:[:U,U:],U:]
[:U,U:] is Relation-like set
[:[:U,U:],U:] is Relation-like set
bool [:[:U,U:],U:] is non empty set
U is set
q1 is Relation-like Function-like set
q11 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable finite-support set
proj2 q11 is finite countable set
U is set
union U is set
q1 is set
q2 is set
Funcs (q1,q2) is functional set
[:q1,q2:] is Relation-like set
bool [:q1,q2:] is non empty Element of bool (bool [:q1,q2:])
bool [:q1,q2:] is non empty set
bool (bool [:q1,q2:]) is non empty set
bool (bool [:q1,q2:]) is non empty set
p is Element of bool (bool [:q1,q2:])
union p is Relation-like q1 -defined q2 -valued Element of bool [:q1,q2:]
U is set
q1 is Relation-like Function-like set
proj1 q1 is set
(proj1 q1) /\ U is set
q1 | U is Relation-like Function-like set
f is set
q11 is set
q1 . f is set
q1 . q11 is set
proj1 (q1 | U) is set
(q1 | U) . f is set
(q1 | U) . q11 is set
f is set
proj1 (q1 | U) is set
q11 is set
(q1 | U) . f is set
(q1 | U) . q11 is set
q1 . f is set
q1 . q11 is set
U is non empty set
[:U,U:] is Relation-like non empty set
[:[:U,U:],U:] is Relation-like non empty set
bool [:[:U,U:],U:] is non empty set
q1 is set
q2 is set
f is Relation-like [:U,U:] -defined U -valued Function-like non empty total quasi_total Element of bool [:[:U,U:],U:]
f | q2 is Relation-like [:U,U:] -defined q2 -defined [:U,U:] -defined U -valued Function-like Element of bool [:[:U,U:],U:]
f | q1 is Relation-like [:U,U:] -defined q1 -defined [:U,U:] -defined U -valued Function-like Element of bool [:[:U,U:],U:]
(f | q2) | q1 is Relation-like [:U,U:] -defined q1 -defined [:U,U:] -defined U -valued Function-like Element of bool [:[:U,U:],U:]
U is set
q1 is set
q2 is complex epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal ext-real non negative countable set
q2 -tuples_on U is functional FinSequence-membered FinSequenceSet of U
f is complex epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal ext-real non negative countable set
f -tuples_on q1 is functional FinSequence-membered FinSequenceSet of q1
(q2 -tuples_on U) /\ (f -tuples_on q1) is set
q11 is set
F is Relation-like NAT -defined Function-like finite q2 -element FinSequence-like FinSubsequence-like countable finite-support set
len F is complex epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal ext-real non negative countable Element of NAT
p is Relation-like NAT -defined Function-like finite f -element FinSequence-like FinSubsequence-like countable finite-support set
len p is complex epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal ext-real non negative countable Element of NAT
U is complex epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal ext-real non negative countable set
Seg U is finite U -element countable Element of bool NAT
{ b1 where b1 is complex epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal ext-real non negative countable Element of NAT : ( 1 <= b1 & b1 <= U ) } is set
q1 is set
U -tuples_on q1 is functional FinSequence-membered FinSequenceSet of q1
Funcs ((Seg U),q1) is functional set
q2 is non empty set
U -tuples_on q2 is functional non empty FinSequence-membered FinSequenceSet of q2
Funcs ((Seg U),q2) is functional non empty FUNCTION_DOMAIN of Seg U,q2
U is set
q1 is set
q1 * is functional non empty FinSequence-membered FinSequenceSet of q1
q2 is complex epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal ext-real non negative countable set
q2 -tuples_on U is functional FinSequence-membered FinSequenceSet of U
(q2 -tuples_on U) /\ (q1 *) is set
q2 -tuples_on q1 is functional FinSequence-membered FinSequenceSet of q1
p is set
C is Relation-like NAT -defined q1 -valued Function-like finite FinSequence-like FinSubsequence-like countable finite-support FinSequence of q1
len C is complex epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal ext-real non negative countable Element of NAT
dom C is finite countable Element of bool NAT
Seg q2 is finite q2 -element countable Element of bool NAT
{ b1 where b1 is complex epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal ext-real non negative countable Element of NAT : ( 1 <= b1 & b1 <= q2 ) } is set
rng C is finite countable Element of bool q1
bool q1 is non empty set
Funcs ((Seg q2),q1) is functional set
U is set
q1 is set
q1 * is functional non empty FinSequence-membered FinSequenceSet of q1
q2 is complex epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal ext-real non negative countable set
q2 -tuples_on U is functional FinSequence-membered FinSequenceSet of U
(q2 -tuples_on U) /\ (q1 *) is set
q2 -tuples_on q1 is functional FinSequence-membered FinSequenceSet of q1
(q2 -tuples_on U) /\ (q2 -tuples_on q1) is set
(q2 -tuples_on U) /\ ((q2 -tuples_on U) /\ (q1 *)) is set
(q2 -tuples_on U) /\ (q2 -tuples_on U) is set
((q2 -tuples_on U) /\ (q2 -tuples_on U)) /\ (q1 *) is set
p is set
C is Relation-like NAT -defined Function-like finite q2 -element FinSequence-like FinSubsequence-like countable finite-support set
f is complex epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal ext-real non negative countable Element of NAT
f -tuples_on q1 is functional FinSequence-membered FinSequenceSet of q1
len C is complex epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal ext-real non negative countable Element of NAT
proj2 C is finite countable set
U is set
q1 is set
Funcs (U,q1) is functional set
q2 is set
Funcs (U,q2) is functional set
(Funcs (U,q1)) /\ (Funcs (U,q2)) is set
q1 /\ q2 is set
Funcs (U,(q1 /\ q2)) is functional set
F is set
p is Relation-like Function-like set
proj1 p is set
proj2 p is set
C is Relation-like Function-like set
proj1 C is set
proj2 C is set
U is set
q1 is set
q1 * is functional non empty FinSequence-membered FinSequenceSet of q1
U /\ q1 is set
q2 is complex epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal ext-real non negative countable set
q2 -tuples_on U is functional FinSequence-membered FinSequenceSet of U
(q2 -tuples_on U) /\ (q1 *) is set
q2 -tuples_on (U /\ q1) is functional FinSequence-membered FinSequenceSet of U /\ q1
Seg q2 is finite q2 -element countable Element of bool NAT
{ b1 where b1 is complex epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal ext-real non negative countable Element of NAT : ( 1 <= b1 & b1 <= q2 ) } is set
Funcs ((Seg q2),(U /\ q1)) is functional set
Funcs ((Seg q2),U) is functional set
Funcs ((Seg q2),q1) is functional set
(Funcs ((Seg q2),U)) /\ (Funcs ((Seg q2),q1)) is set
(q2 -tuples_on U) /\ (Funcs ((Seg q2),q1)) is set
q2 -tuples_on q1 is functional FinSequence-membered FinSequenceSet of q1
(q2 -tuples_on U) /\ (q2 -tuples_on q1) is set
U is set
q1 is set
U /\ q1 is set
q2 is complex epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal ext-real non negative countable set
q2 -tuples_on (U /\ q1) is functional FinSequence-membered FinSequenceSet of U /\ q1
q2 -tuples_on U is functional FinSequence-membered FinSequenceSet of U
q2 -tuples_on q1 is functional FinSequence-membered FinSequenceSet of q1
(q2 -tuples_on U) /\ (q2 -tuples_on q1) is set
q1 * is functional non empty FinSequence-membered FinSequenceSet of q1
(q2 -tuples_on U) /\ (q1 *) is set
U is non empty set
U -concatenation is Relation-like [:(U *),(U *):] -defined U * -valued Function-like non empty total quasi_total Function-yielding V159() Element of bool [:[:(U *),(U *):],(U *):]
U * is functional non empty FinSequence-membered FinSequenceSet of U
[:(U *),(U *):] is Relation-like non empty set
[:[:(U *),(U *):],(U *):] is Relation-like non empty set
bool [:[:(U *),(U *):],(U *):] is non empty set
q1 is Relation-like NAT -defined U -valued Function-like finite FinSequence-like FinSubsequence-like countable finite-support FinSequence of U
q2 is Relation-like NAT -defined U -valued Function-like finite FinSequence-like FinSubsequence-like countable finite-support FinSequence of U
(U -concatenation) . (q1,q2) is set
[q1,q2] is non empty V15() set
(U -concatenation) . [q1,q2] is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable finite-support set
q1 ^ q2 is Relation-like NAT -defined U -valued Function-like finite FinSequence-like FinSubsequence-like countable finite-support Element of U *
U *+^ is non empty strict V94() associative constituted-Functions constituted-FinSeqs left-cancelable right-cancelable V153() uniquely-decomposable multMagma
the U1 of (U *+^) is set
f is Relation-like NAT -defined U -valued Function-like finite FinSequence-like FinSubsequence-like countable finite-support Element of U *
q11 is Relation-like NAT -defined U -valued Function-like finite FinSequence-like FinSubsequence-like countable finite-support Element of U *
the multF of (U *+^) is Relation-like [: the U1 of (U *+^), the U1 of (U *+^):] -defined the U1 of (U *+^) -valued Function-like quasi_total Element of bool [:[: the U1 of (U *+^), the U1 of (U *+^):], the U1 of (U *+^):]
[: the U1 of (U *+^), the U1 of (U *+^):] is Relation-like set
[:[: the U1 of (U *+^), the U1 of (U *+^):], the U1 of (U *+^):] is Relation-like set
bool [:[: the U1 of (U *+^), the U1 of (U *+^):], the U1 of (U *+^):] is non empty set
F is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable finite-support Element of the U1 of (U *+^)
p is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable finite-support Element of the U1 of (U *+^)
F ^ p is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable finite-support set
F [*] p is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable finite-support Element of the U1 of (U *+^)
(U -concatenation) . (F,p) is set
[F,p] is non empty V15() set
(U -concatenation) . [F,p] is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable finite-support set
U is non empty set
U -concatenation is Relation-like [:(U *),(U *):] -defined U * -valued Function-like non empty total quasi_total Function-yielding V159() Element of bool [:[:(U *),(U *):],(U *):]
U * is functional non empty FinSequence-membered FinSequenceSet of U
[:(U *),(U *):] is Relation-like non empty set
[:[:(U *),(U *):],(U *):] is Relation-like non empty set
bool [:[:(U *),(U *):],(U *):] is non empty set
q1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable finite-support set
q2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable finite-support set
(U -concatenation) . (q1,q2) is set
[q1,q2] is non empty V15() set
(U -concatenation) . [q1,q2] is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable finite-support set
q1 ^ q2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable finite-support set
q11 is Relation-like NAT -defined U -valued Function-like finite FinSequence-like FinSubsequence-like countable finite-support FinSequence of U
F is Relation-like NAT -defined U -valued Function-like finite FinSequence-like FinSubsequence-like countable finite-support FinSequence of U
(U -concatenation) . (q11,F) is set
[q11,F] is non empty V15() set
(U -concatenation) . [q11,F] is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable finite-support set
q11 ^ F is Relation-like NAT -defined U -valued Function-like finite FinSequence-like FinSubsequence-like countable finite-support Element of U *
U is non empty set
U * is functional non empty FinSequence-membered FinSequenceSet of U
(U *) \ {{}} is functional FinSequence-membered Element of bool (U *)
bool (U *) is non empty set
q1 is set
U is non empty set
[:U,U:] is Relation-like non empty set
[:[:U,U:],U:] is Relation-like non empty set
bool [:[:U,U:],U:] is non empty set
q1 is set
q2 is set
f is Relation-like [:U,U:] -defined U -valued Function-like non empty total quasi_total Element of bool [:[:U,U:],U:]
[:q1,U:] is Relation-like set
[:q2,U:] is Relation-like set
U is non empty set
[:U,U:] is Relation-like non empty set
[:[:U,U:],U:] is Relation-like non empty set
bool [:[:U,U:],U:] is non empty set
q1 is Relation-like [:U,U:] -defined U -valued Function-like non empty total quasi_total Element of bool [:[:U,U:],U:]
[:{},U:] is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty trivial complex epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural real integer finite finite-yielding finite-membered cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative Function-yielding V159() FuncSeq-like Cardinal-yielding countable FinSequence-yielding finite-support set
q2 is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty trivial complex epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural real integer finite finite-yielding finite-membered cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative Function-yielding V159() FuncSeq-like Cardinal-yielding countable FinSequence-yielding finite-support set
q1 | q2 is Relation-like non-empty empty-yielding NAT -defined [:U,U:] -defined q2 -defined [:U,U:] -defined U -valued Function-like one-to-one constant functional empty trivial proper complex epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural real integer finite finite-yielding finite-membered cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative Function-yielding V159() FuncSeq-like Cardinal-yielding countable FinSequence-yielding finite-support Element of bool [:[:U,U:],U:]
U is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable finite-support set
q1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable finite-support set
<:U,q1:> is Relation-like Function-like set
proj1 <:U,q1:> is set
len U is complex epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal ext-real non negative countable Element of NAT
len q1 is complex epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal ext-real non negative countable Element of NAT
min ((len U),(len q1)) is complex epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal ext-real non negative countable set
Seg (min ((len U),(len q1))) is finite min ((len U),(len q1)) -element countable Element of bool NAT
{ b1 where b1 is complex epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal ext-real non negative countable Element of NAT : ( 1 <= b1 & b1 <= min ((len U),(len q1)) ) } is set
dom U is finite countable Element of bool NAT
dom q1 is finite countable Element of bool NAT
(dom U) /\ (dom q1) is finite countable Element of bool NAT
Seg (len U) is finite len U -element countable Element of bool NAT
{ b1 where b1 is complex epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal ext-real non negative countable Element of NAT : ( 1 <= b1 & b1 <= len U ) } is set
(Seg (len U)) /\ (dom q1) is finite countable Element of bool NAT
Seg (len q1) is finite len q1 -element countable Element of bool NAT
{ b1 where b1 is complex epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal ext-real non negative countable Element of NAT : ( 1 <= b1 & b1 <= len q1 ) } is set
(Seg (len U)) /\ (Seg (len q1)) is finite countable Element of bool NAT
U is non empty set
[:U,U:] is Relation-like non empty set
[:[:U,U:],U:] is Relation-like non empty set
bool [:[:U,U:],U:] is non empty set
(U) is Relation-like [:U,U:] -defined U -valued Function-like non empty total quasi_total Element of bool [:[:U,U:],U:]
pr1 (U,U) is Relation-like [:U,U:] -defined U -valued Function-like non empty total quasi_total Element of bool [:[:U,U:],U:]
q1 is Element of U
q2 is Element of U
f is Element of U
(U) . (q2,f) is Element of U
[q2,f] is non empty V15() set
(U) . [q2,f] is set
(U) . (q1,((U) . (q2,f))) is Element of U
[q1,((U) . (q2,f))] is non empty V15() set
(U) . [q1,((U) . (q2,f))] is set
(U) . (q1,q2) is Element of U
[q1,q2] is non empty V15() set
(U) . [q1,q2] is set
(U) . (((U) . (q1,q2)),f) is Element of U
[((U) . (q1,q2)),f] is non empty V15() set
(U) . [((U) . (q1,q2)),f] is set
(U) . (q1,f) is Element of U
[q1,f] is non empty V15() set
(U) . [q1,f] is set
q1 is Relation-like [:U,U:] -defined U -valued Function-like non empty total quasi_total Element of bool [:[:U,U:],U:]
U is set
[:U,U:] is Relation-like set
[:[:U,U:],U:] is Relation-like set
bool [:[:U,U:],U:] is non empty set
q1 is non empty set
(q1) is Relation-like [:q1,q1:] -defined q1 -valued Function-like non empty total quasi_total associative Element of bool [:[:q1,q1:],q1:]
[:q1,q1:] is Relation-like non empty set
[:[:q1,q1:],q1:] is Relation-like non empty set
bool [:[:q1,q1:],q1:] is non empty set
pr1 (q1,q1) is Relation-like [:q1,q1:] -defined q1 -valued Function-like non empty total quasi_total Element of bool [:[:q1,q1:],q1:]
q2 is Relation-like [:U,U:] -defined U -valued Function-like quasi_total Element of bool [:[:U,U:],U:]
[:[:{},{}:],{}:] is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty trivial complex epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural real integer finite finite-yielding finite-membered cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative Function-yielding V159() FuncSeq-like Cardinal-yielding countable FinSequence-yielding finite-support set
bool [:[:{},{}:],{}:] is non empty finite finite-membered countable set
the Relation-like non-empty empty-yielding [:{},{}:] -defined {} -valued Function-like one-to-one constant functional empty trivial non proper total quasi_total complex epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural real integer finite finite-yielding finite-membered cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative commutative associative Function-yielding V159() FuncSeq-like Cardinal-yielding countable FinSequence-yielding finite-support Element of bool [:[:{},{}:],{}:] is Relation-like non-empty empty-yielding [:{},{}:] -defined {} -valued Function-like one-to-one constant functional empty trivial non proper total quasi_total complex epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural real integer finite finite-yielding finite-membered cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative commutative associative Function-yielding V159() FuncSeq-like Cardinal-yielding countable FinSequence-yielding finite-support Element of bool [:[:{},{}:],{}:]
q1 is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty trivial complex epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural real integer finite finite-yielding finite-membered cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative Function-yielding V159() FuncSeq-like Cardinal-yielding countable FinSequence-yielding finite-support set
[:q1,q1:] is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty trivial complex epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural real integer finite finite-yielding finite-membered cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative Function-yielding V159() FuncSeq-like Cardinal-yielding countable FinSequence-yielding finite-support set
[:[:q1,q1:],q1:] is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty trivial complex epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural real integer finite finite-yielding finite-membered cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative Function-yielding V159() FuncSeq-like Cardinal-yielding countable FinSequence-yielding finite-support set
bool [:[:q1,q1:],q1:] is non empty finite finite-membered countable set
U is set
bool U is non empty set
q1 is Element of bool U
q1 * is functional non empty FinSequence-membered set
U * is functional non empty FinSequence-membered FinSequenceSet of U
bool (U *) is non empty set
U is non empty set
U * is functional non empty FinSequence-membered FinSequenceSet of U
[:(U *),(U *):] is Relation-like non empty set
[:[:(U *),(U *):],(U *):] is Relation-like non empty set
bool [:[:(U *),(U *):],(U *):] is non empty set
U -concatenation is Relation-like [:(U *),(U *):] -defined U * -valued Function-like non empty total quasi_total Function-yielding V159() Element of bool [:[:(U *),(U *):],(U *):]
q1 is Relation-like [:(U *),(U *):] -defined U * -valued Function-like non empty total quasi_total Function-yielding V159() Element of bool [:[:(U *),(U *):],(U *):]
U is non empty set
U * is functional non empty FinSequence-membered FinSequenceSet of U
(U *) \ {{}} is functional FinSequence-membered Element of bool (U *)
bool (U *) is non empty set
the Element of U is Element of U
<* the Element of U*> is Relation-like NAT -defined U -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like countable finite-support FinSequence of U
[1, the Element of U] is non empty V15() set
{[1, the Element of U]} is Relation-like Function-like constant non empty trivial finite 1 -element with_non-empty_elements non empty-membered countable finite-support set
U is non empty set
U * is functional non empty FinSequence-membered FinSequenceSet of U
q1 is complex epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal ext-real non negative countable set
the Relation-like NAT -defined U -valued Function-like finite q1 -element FinSequence-like FinSubsequence-like countable finite-support FinSequence of U is Relation-like NAT -defined U -valued Function-like finite q1 -element FinSequence-like FinSubsequence-like countable finite-support FinSequence of U
f is Relation-like NAT -defined U -valued Function-like finite FinSequence-like FinSubsequence-like countable finite-support Element of U *
U is set
q1 is Relation-like Function-like set
proj1 q1 is set
U /\ (proj1 q1) is set
q2 is set
f is set
q1 . q2 is set
q1 . f is set
U is non empty set
[:U,U:] is Relation-like non empty set
[:[:U,U:],U:] is Relation-like non empty set
bool [:[:U,U:],U:] is non empty set
q1 is Relation-like [:U,U:] -defined U -valued Function-like non empty total quasi_total Element of bool [:[:U,U:],U:]
U is Relation-like Function-like set
q1 is set
{q1} is non empty trivial finite 1 -element countable set
U | {q1} is Relation-like Function-like finite countable finite-support set
proj1 U is set
U . q1 is set
q1 .--> (U . q1) is Relation-like {q1} -defined Function-like one-to-one constant non empty trivial finite 1 -element countable finite-support set
{q1} --> (U . q1) is Relation-like {q1} -defined {(U . q1)} -valued Function-like constant non empty total quasi_total finite countable finite-support Element of bool [:{q1},{(U . q1)}:]
{(U . q1)} is non empty trivial finite 1 -element countable set
[:{q1},{(U . q1)}:] is Relation-like non empty finite countable set
bool [:{q1},{(U . q1)}:] is non empty finite finite-membered countable set
proj1 U is set
f is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty trivial complex epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural real integer finite finite-yielding finite-membered cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative Function-yielding V159() FuncSeq-like Cardinal-yielding countable FinSequence-yielding finite-support set
proj1 U is set
U is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty trivial complex epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural real integer finite finite-yielding finite-membered cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative Function-yielding V159() FuncSeq-like Cardinal-yielding countable FinSequence-yielding finite-support set
U * is functional non empty FinSequence-membered FinSequenceSet of U
{U} is functional non empty trivial finite finite-membered 1 -element with_common_domain countable set
U is set
U is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty trivial complex epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural real integer finite finite-yielding finite-membered cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative Function-yielding V159() FuncSeq-like empty-membered Cardinal-yielding countable FinSequence-yielding finite-support set
{U} is functional non empty trivial finite finite-membered 1 -element with_common_domain countable set
U * is functional non empty FinSequence-membered FinSequenceSet of U
q1 is non empty set
q1 is non empty complex epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal ext-real positive non negative countable set
U is non empty set
q1 -tuples_on U is functional non empty FinSequence-membered FinSequenceSet of U
len {} is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty trivial complex epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural real integer finite finite-yielding finite-membered cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative Function-yielding V159() FuncSeq-like empty-membered Cardinal-yielding countable FinSequence-yielding finite-support Element of NAT
U is empty-membered set
bool U is non empty set
q1 is Element of bool U
q2 is non empty set
q1 is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty trivial complex epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural real integer finite finite-yielding finite-membered cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative Function-yielding V159() FuncSeq-like empty-membered Cardinal-yielding countable FinSequence-yielding finite-support set
U is set
q1 -tuples_on U is functional FinSequence-membered FinSequenceSet of U
q2 is set
q1 is non empty complex epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal ext-real positive non negative countable set
U is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty trivial complex epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural real integer finite finite-yielding finite-membered cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative Function-yielding V159() FuncSeq-like empty-membered Cardinal-yielding countable FinSequence-yielding finite-support set
q1 -tuples_on U is functional FinSequence-membered FinSequenceSet of U
U is non empty set
[:U,U:] is Relation-like non empty set
[:[:U,U:],U:] is Relation-like non empty set
bool [:[:U,U:],U:] is non empty set
q1 is Relation-like [:U,U:] -defined U -valued Function-like non empty total quasi_total Element of bool [:[:U,U:],U:]
q2 is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty trivial complex epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural real integer finite finite-yielding finite-membered cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative Function-yielding V159() FuncSeq-like empty-membered Cardinal-yielding countable FinSequence-yielding finite-support set
q2 /\ q1 is Relation-like NAT -defined [:U,U:] -defined U -valued finite countable Element of bool [:[:U,U:],U:]
U is non empty set
q1 is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty trivial complex epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural real integer finite finite-yielding finite-membered cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative Function-yielding V159() FuncSeq-like empty-membered Cardinal-yielding countable FinSequence-yielding finite-support set
q1 /\ U is Relation-like finite countable set
U -concatenation is Relation-like [:(U *),(U *):] -defined U * -valued Function-like non empty total quasi_total associative Function-yielding V159() Element of bool [:[:(U *),(U *):],(U *):]
U * is functional non empty FinSequence-membered FinSequenceSet of U
[:(U *),(U *):] is Relation-like non empty set
[:[:(U *),(U *):],(U *):] is Relation-like non empty set
bool [:[:(U *),(U *):],(U *):] is non empty set
q1 /\ (U -concatenation) is Relation-like NAT -defined [:(U *),(U *):] -defined U * -valued finite countable (U * ,U -concatenation ) Element of bool [:[:(U *),(U *):],(U *):]
U is non empty set
{} /\ U is Relation-like finite countable (U) set
U is non empty set
[:U,U:] is Relation-like non empty set
[:[:U,U:],U:] is Relation-like non empty set
bool [:[:U,U:],U:] is non empty set
q2 is Relation-like NAT -defined U -valued Function-like finite FinSequence-like FinSubsequence-like countable finite-support FinSequence of U
q2 . 1 is set
q1 is Relation-like [:U,U:] -defined U -valued Function-like non empty total quasi_total Element of bool [:[:U,U:],U:]
f is Relation-like Function-like set
proj1 f is set
f . {} is set
q11 is complex epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal ext-real non negative countable set
q11 + 1 is non empty complex epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal ext-real positive non negative countable set
f . (q11 + 1) is set
f . q11 is set
q11 + 2 is non empty complex epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal ext-real positive non negative countable set
q2 . (q11 + 2) is set
q1 . ((f . q11),(q2 . (q11 + 2))) is set
[(f . q11),(q2 . (q11 + 2))] is non empty V15() set
q1 . [(f . q11),(q2 . (q11 + 2))] is set
f is Relation-like Function-like set
proj1 f is set
f . {} is set
q11 is Relation-like Function-like set
proj1 q11 is set
q11 . {} is set
F is complex epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal ext-real non negative countable set
F + 1 is non empty complex epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal ext-real positive non negative countable set
f . (F + 1) is set
f . F is set
F + 2 is non empty complex epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal ext-real positive non negative countable set
q2 . (F + 2) is set
q1 . ((f . F),(q2 . (F + 2))) is set
[(f . F),(q2 . (F + 2))] is non empty V15() set
q1 . [(f . F),(q2 . (F + 2))] is set
F is complex epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal ext-real non negative countable set
F + 1 is non empty complex epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal ext-real positive non negative countable set
q11 . (F + 1) is set
q11 . F is set
F + 2 is non empty complex epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal ext-real positive non negative countable set
q2 . (F + 2) is set
q1 . ((q11 . F),(q2 . (F + 2))) is set
[(q11 . F),(q2 . (F + 2))] is non empty V15() set
q1 . [(q11 . F),(q2 . (F + 2))] is set
U is non empty set
[:U,U:] is Relation-like non empty set
[:[:U,U:],U:] is Relation-like non empty set
bool [:[:U,U:],U:] is non empty set
q1 is Relation-like [:U,U:] -defined U -valued Function-like non empty total quasi_total Element of bool [:[:U,U:],U:]
q2 is Relation-like NAT -defined U -valued Function-like finite FinSequence-like FinSubsequence-like countable finite-support FinSequence of U
len q2 is complex epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal ext-real non negative countable Element of NAT
(U,q1,q2) is Relation-like Function-like set
{} + 1 is non empty complex epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal ext-real positive non negative countable set
(U,q1,q2) . {} is set
Seg (len q2) is finite len q2 -element countable Element of bool NAT
{ b1 where b1 is complex epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal ext-real non negative countable Element of NAT : ( 1 <= b1 & b1 <= len q2 ) } is set
dom q2 is finite countable Element of bool NAT
q2 . 1 is set
rng q2 is finite countable Element of bool U
bool U is non empty set
f is complex epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal ext-real non negative countable set
f + 1 is non empty complex epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal ext-real positive non negative countable set
(U,q1,q2) . f is set
(f + 1) + 1 is non empty complex epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal ext-real positive non negative countable set
(U,q1,q2) . (f + 1) is set
f + 2 is non empty complex epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal ext-real positive non negative countable set
Seg (len q2) is finite len q2 -element countable Element of bool NAT
{ b1 where b1 is complex epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal ext-real non negative countable Element of NAT : ( 1 <= b1 & b1 <= len q2 ) } is set
dom q2 is finite countable Element of bool NAT
q2 . (f + 2) is set
rng q2 is finite countable Element of bool U
bool U is non empty set
[((U,q1,q2) . f),(q2 . (f + 2))] is non empty V15() set
q1 . (((U,q1,q2) . f),(q2 . (f + 2))) is set
q1 . [((U,q1,q2) . f),(q2 . (f + 2))] is set
f is complex epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal ext-real non negative countable set
q2 | f is Relation-like NAT -defined U -valued Function-like finite FinSequence-like FinSubsequence-like countable finite-support FinSequence of U
Seg f is finite f -element countable Element of bool NAT
{ b1 where b1 is complex epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal ext-real non negative countable Element of NAT : ( 1 <= b1 & b1 <= f ) } is set
q2 | (Seg f) is Relation-like NAT -defined Seg f -defined NAT -defined U -valued Function-like finite FinSequence-like FinSubsequence-like countable finite-support set
(U,q1,(q2 | f)) is Relation-like Function-like set
(U,q1,(q2 | f)) . {} is set
(q2 | f) . 1 is set
q2 . 1 is set
f is complex epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal ext-real non negative countable set
f + 1 is non empty complex epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal ext-real positive non negative countable set
(U,q1,q2) . f is set
(f + 1) + 1 is non empty complex epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal ext-real positive non negative countable set
(U,q1,q2) . (f + 1) is set
q11 is complex epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal ext-real non negative countable set
q2 | q11 is Relation-like NAT -defined U -valued Function-like finite FinSequence-like FinSubsequence-like countable finite-support FinSequence of U
Seg q11 is finite q11 -element countable Element of bool NAT
{ b1 where b1 is complex epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal ext-real non negative countable Element of NAT : ( 1 <= b1 & b1 <= q11 ) } is set
q2 | (Seg q11) is Relation-like NAT -defined Seg q11 -defined NAT -defined U -valued Function-like finite FinSequence-like FinSubsequence-like countable finite-support set
(U,q1,(q2 | q11)) is Relation-like Function-like set
(U,q1,(q2 | q11)) . (f + 1) is set
f + 2 is non empty complex epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal ext-real positive non negative countable set
(U,q1,(q2 | q11)) . f is set
(q2 | q11) . (f + 2) is set
q1 . (((U,q1,(q2 | q11)) . f),((q2 | q11) . (f + 2))) is set
[((U,q1,(q2 | q11)) . f),((q2 | q11) . (f + 2))] is non empty V15() set
q1 . [((U,q1,(q2 | q11)) . f),((q2 | q11) . (f + 2))] is set
q1 . (((U,q1,q2) . f),((q2 | q11) . (f + 2))) is set
[((U,q1,q2) . f),((q2 | q11) . (f + 2))] is non empty V15() set
q1 . [((U,q1,q2) . f),((q2 | q11) . (f + 2))] is set
q2 . (f + 2) is set
q1 . (((U,q1,q2) . f),(q2 . (f + 2))) is set
[((U,q1,q2) . f),(q2 . (f + 2))] is non empty V15() set
q1 . [((U,q1,q2) . f),(q2 . (f + 2))] is set
f is complex epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal ext-real non negative countable set
q2 | f is Relation-like NAT -defined U -valued Function-like finite FinSequence-like FinSubsequence-like countable finite-support FinSequence of U
Seg f is finite f -element countable Element of bool NAT
{ b1 where b1 is complex epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal ext-real non negative countable Element of NAT : ( 1 <= b1 & b1 <= f ) } is set
q2 | (Seg f) is Relation-like NAT -defined Seg f -defined NAT -defined U -valued Function-like finite FinSequence-like FinSubsequence-like countable finite-support set
(U,q1,(q2 | f)) is Relation-like Function-like set
(U,q1,(q2 | f)) . {} is set
f is complex epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal ext-real non negative countable set
f + 1 is non empty complex epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal ext-real positive non negative countable set
(U,q1,q2) . f is set
(f + 1) + 1 is non empty complex epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal ext-real positive non negative countable set
q11 is complex epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal ext-real non negative countable set
q2 | q11 is Relation-like NAT -defined U -valued Function-like finite FinSequence-like FinSubsequence-like countable finite-support FinSequence of U
Seg q11 is finite q11 -element countable Element of bool NAT
{ b1 where b1 is complex epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal ext-real non negative countable Element of NAT : ( 1 <= b1 & b1 <= q11 ) } is set
q2 | (Seg q11) is Relation-like NAT -defined Seg q11 -defined NAT -defined U -valued Function-like finite FinSequence-like FinSubsequence-like countable finite-support set
(U,q1,(q2 | q11)) is Relation-like Function-like set
(U,q1,(q2 | q11)) . (f + 1) is set
(U,q1,q2) . (f + 1) is set
f is complex epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal ext-real non negative countable set
f + 1 is non empty complex epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal ext-real positive non negative countable set
(U,q1,q2) . f is set
q11 is complex epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal ext-real non negative countable set
q11 + 1 is non empty complex epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal ext-real positive non negative countable set
F is complex epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal ext-real non negative countable set
q2 | F is Relation-like NAT -defined U -valued Function-like finite FinSequence-like FinSubsequence-like countable finite-support FinSequence of U
Seg F is finite F -element countable Element of bool NAT
{ b1 where b1 is complex epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal ext-real non negative countable Element of NAT : ( 1 <= b1 & b1 <= F ) } is set
q2 | (Seg F) is Relation-like NAT -defined Seg F -defined NAT -defined U -valued Function-like finite FinSequence-like FinSubsequence-like countable finite-support set
(U,q1,(q2 | F)) is Relation-like Function-like set
(U,q1,(q2 | F)) . q11 is set
(U,q1,q2) . q11 is set
U is non empty set
[:U,U:] is Relation-like non empty set
[:[:U,U:],U:] is Relation-like non empty set
bool [:[:U,U:],U:] is non empty set
U * is functional non empty FinSequence-membered FinSequenceSet of U
(U *) \ {{}} is functional non empty FinSequence-membered Element of bool (U *)
bool (U *) is non empty set
q1 is Relation-like [:U,U:] -defined U -valued Function-like non empty total quasi_total Element of bool [:[:U,U:],U:]
q2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable finite-support Element of (U *) \ {{}}
(U,q1,q2) is Relation-like Function-like set
U is non empty set
[:U,U:] is Relation-like non empty set
[:[:U,U:],U:] is Relation-like non empty set
bool [:[:U,U:],U:] is non empty set
U * is functional non empty FinSequence-membered FinSequenceSet of U
(U *) \ {{}} is functional non empty FinSequence-membered Element of bool (U *)
bool (U *) is non empty set
[:((U *) \ {{}}),U:] is Relation-like non empty set
bool [:((U *) \ {{}}),U:] is non empty set
q1 is Relation-like [:U,U:] -defined U -valued Function-like non empty total quasi_total Element of bool [:[:U,U:],U:]
q2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable finite-support Element of (U *) \ {{}}
(U,q1,q2) is Relation-like Function-like set
(U,q1,q2) is Relation-like Function-like set
len q2 is complex epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal ext-real non negative countable Element of NAT
(len q2) - 1 is complex real integer finite ext-real countable set
(U,q1,q2) . ((len q2) - 1) is set
f is Relation-like NAT -defined U -valued Function-like finite FinSequence-like FinSubsequence-like countable finite-support Element of U *
len f is complex epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal ext-real non negative countable Element of NAT
(len f) - 1 is complex real integer finite ext-real countable set
q11 is complex epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal ext-real non negative countable set
q11 + 1 is non empty complex epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal ext-real positive non negative countable set
(U,q1,f) is Relation-like Function-like set
(U,q1,f) . q11 is set
F is Element of U
q2 is Relation-like (U *) \ {{}} -defined U -valued Function-like non empty total quasi_total Element of bool [:((U *) \ {{}}),U:]
f is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable finite-support Element of (U *) \ {{}}
q2 . f is Element of U
(U,q1,f) is Relation-like Function-like set
(U,q1,f) is Relation-like Function-like set
len f is complex epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal ext-real non negative countable Element of NAT
(len f) - 1 is complex real integer finite ext-real countable set
(U,q1,f) . ((len f) - 1) is set
q2 is Relation-like (U *) \ {{}} -defined U -valued Function-like non empty total quasi_total Element of bool [:((U *) \ {{}}),U:]
f is Relation-like (U *) \ {{}} -defined U -valued Function-like non empty total quasi_total Element of bool [:((U *) \ {{}}),U:]
dom q2 is functional non empty FinSequence-membered Element of bool ((U *) \ {{}})
bool ((U *) \ {{}}) is non empty set
dom f is functional non empty FinSequence-membered Element of bool ((U *) \ {{}})
q11 is set
q2 . q11 is set
F is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable finite-support Element of (U *) \ {{}}
(U,q1,F) is Relation-like Function-like set
(U,q1,F) is Relation-like Function-like set
len F is complex epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal ext-real non negative countable Element of NAT
(len F) - 1 is complex real integer finite ext-real countable set
(U,q1,F) . ((len F) - 1) is set
f . q11 is set
U is non empty set
[:U,U:] is Relation-like non empty set
[:[:U,U:],U:] is Relation-like non empty set
bool [:[:U,U:],U:] is non empty set
q1 is Relation-like [:U,U:] -defined U -valued Function-like non empty total quasi_total Element of bool [:[:U,U:],U:]
(U,q1) is Relation-like (U *) \ {{}} -defined U -valued Function-like non empty total quasi_total Element of bool [:((U *) \ {{}}),U:]
U * is functional non empty FinSequence-membered FinSequenceSet of U
(U *) \ {{}} is functional non empty FinSequence-membered Element of bool (U *)
bool (U *) is non empty set
[:((U *) \ {{}}),U:] is Relation-like non empty set
bool [:((U *) \ {{}}),U:] is non empty set
f is Relation-like NAT -defined U -valued Function-like non empty finite FinSequence-like FinSubsequence-like countable finite-support FinSequence of U
(U,q1) . f is set
q11 is Element of U
<*q11*> is Relation-like NAT -defined U -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like countable finite-support FinSequence of U
[1,q11] is non empty V15() set
{[1,q11]} is Relation-like Function-like constant non empty trivial finite 1 -element with_non-empty_elements non empty-membered countable finite-support set
(U,q1) . <*q11*> is set
f ^ <*q11*> is Relation-like NAT -defined U -valued Function-like non empty finite FinSequence-like FinSubsequence-like countable finite-support Element of U *
(U,q1) . (f ^ <*q11*>) is set
q1 . (((U,q1) . f),q11) is set
[((U,q1) . f),q11] is non empty V15() set
q1 . [((U,q1) . f),q11] is set
len f is non empty complex epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal ext-real positive non negative countable Element of NAT
F is complex epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal ext-real non negative countable set
F + 1 is non empty complex epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal ext-real positive non negative countable set
dom <*q11*> is non empty trivial finite 1 -element countable Element of bool NAT
C is Relation-like NAT -defined U -valued Function-like non empty finite FinSequence-like FinSubsequence-like countable finite-support FinSequence of U
(len f) + 1 is non empty complex epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal ext-real positive non negative countable set
C . ((len f) + 1) is set
<*q11*> . 1 is set
C | (len f) is Relation-like NAT -defined U -valued Function-like finite FinSequence-like FinSubsequence-like countable finite-support FinSequence of U
Seg (len f) is non empty finite len f -element countable Element of bool NAT
{ b1 where b1 is complex epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal ext-real non negative countable Element of NAT : ( 1 <= b1 & b1 <= len f ) } is set
C | (Seg (len f)) is Relation-like NAT -defined Seg (len f) -defined NAT -defined U -valued Function-like finite FinSequence-like FinSubsequence-like countable finite-support set
f | (len f) is Relation-like NAT -defined U -valued Function-like finite FinSequence-like FinSubsequence-like countable finite-support FinSequence of U
f | (Seg (len f)) is Relation-like NAT -defined Seg (len f) -defined NAT -defined U -valued Function-like finite FinSequence-like FinSubsequence-like countable finite-support set
len <*q11*> is non empty complex epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal ext-real positive non negative countable Element of NAT
len C is non empty complex epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal ext-real positive non negative countable Element of NAT
y1 is Relation-like NAT -defined U -valued Function-like non empty finite FinSequence-like FinSubsequence-like countable finite-support FinSequence of U
x is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable finite-support Element of (U *) \ {{}}
len x is complex epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal ext-real non negative countable Element of NAT
(len x) - 1 is complex real integer finite ext-real countable set
(U,q1) . x is Element of U
(U,q1,x) is Relation-like Function-like set
(U,q1,x) is Relation-like Function-like set
(U,q1,x) . {} is set
x . 1 is set
y is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable finite-support Element of (U *) \ {{}}
(U,q1) . y is Element of U
(U,q1,y) is Relation-like Function-like set
(U,q1,y) is Relation-like Function-like set
len y is complex epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal ext-real non negative countable Element of NAT
(len y) - 1 is complex real integer finite ext-real countable set
(U,q1,y) . ((len y) - 1) is set
(U,q1,y) . F is set
F + 2 is non empty complex epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal ext-real positive non negative countable set
y . (F + 2) is set
q1 . (((U,q1,y) . F),(y . (F + 2))) is set
[((U,q1,y) . F),(y . (F + 2))] is non empty V15() set
q1 . [((U,q1,y) . F),(y . (F + 2))] is set
p is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable finite-support Element of (U *) \ {{}}
(U,q1,p) is Relation-like Function-like set
(U,q1,p) is Relation-like Function-like set
(len f) - 1 is complex real integer finite ext-real countable set
(U,q1,p) . ((len f) - 1) is set
y . ((len f) + 1) is set
q1 . (((U,q1,p) . ((len f) - 1)),(y . ((len f) + 1))) is set
[((U,q1,p) . ((len f) - 1)),(y . ((len f) + 1))] is non empty V15() set
q1 . [((U,q1,p) . ((len f) - 1)),(y . ((len f) + 1))] is set
(U,q1) . p is Element of U
q1 . (((U,q1) . p),q11) is Element of U
[((U,q1) . p),q11] is non empty V15() set
q1 . [((U,q1) . p),q11] is set
U is non empty set
[:U,U:] is Relation-like non empty set
[:[:U,U:],U:] is Relation-like non empty set
bool [:[:U,U:],U:] is non empty set
q1 is Relation-like [:U,U:] -defined U -valued Function-like non empty total quasi_total Element of bool [:[:U,U:],U:]
dom q1 is Relation-like U -defined U -valued non empty Element of bool [:U,U:]
bool [:U,U:] is non empty set
q2 is set
[:q2,U:] is Relation-like set
q2 /\ U is set
f is set
q11 is set
F is set
p is set
q1 . (f,F) is set
[f,F] is non empty V15() set
q1 . [f,F] is set
q1 . (q11,p) is set
[q11,p] is non empty V15() set
q1 . [q11,p] is set
U /\ U is set
[:(q2 /\ U),(U /\ U):] is Relation-like set
[:q2,U:] /\ [:U,U:] is Relation-like set
f is set
[:q2,U:] /\ (dom q1) is Relation-like U -defined U -valued Element of bool [:U,U:]
q11 is set
q1 . f is set
q1 . q11 is set
U /\ U is set
[:(q2 /\ U),(U /\ U):] is Relation-like set
F is set
p is set
[F,p] is non empty V15() set
C is set
y1 is set
[C,y1] is non empty V15() set
q1 . (F,p) is set
q1 . [F,p] is set
q1 . (C,y1) is set
q1 . [C,y1] is set
U is non empty set
[:U,U:] is Relation-like non empty set
[:[:U,U:],U:] is Relation-like non empty set
bool [:[:U,U:],U:] is non empty set
q1 is Relation-like [:U,U:] -defined U -valued Function-like non empty total quasi_total Element of bool [:[:U,U:],U:]
q2 is set
q2 /\ U is set
[:q2,U:] is Relation-like set
f is set
q11 is set
F is set
p is set
q1 . (f,F) is set
[f,F] is non empty V15() set
q1 . [f,F] is set
q1 . (q11,p) is set
[q11,p] is non empty V15() set
q1 . [q11,p] is set
[:q2,U:] is Relation-like set
U is non empty set
[:U,U:] is Relation-like non empty set
[:[:U,U:],U:] is Relation-like non empty set
bool [:[:U,U:],U:] is non empty set
q1 is Relation-like [:U,U:] -defined U -valued Function-like non empty total quasi_total Element of bool [:[:U,U:],U:]
(U,q1) is Relation-like (U *) \ {{}} -defined U -valued Function-like non empty total quasi_total Element of bool [:((U *) \ {{}}),U:]
U * is functional non empty FinSequence-membered FinSequenceSet of U
(U *) \ {{}} is functional non empty FinSequence-membered Element of bool (U *)
bool (U *) is non empty set
[:((U *) \ {{}}),U:] is Relation-like non empty set
bool [:((U *) \ {{}}),U:] is non empty set
f is Element of U
<*f*> is Relation-like NAT -defined U -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like countable finite-support FinSequence of U
[1,f] is non empty V15() set
{[1,f]} is Relation-like Function-like constant non empty trivial finite 1 -element with_non-empty_elements non empty-membered countable finite-support set
{} + 1 is non empty complex epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal ext-real positive non negative countable set
({} + 1) -tuples_on U is functional non empty FinSequence-membered with_non-empty_elements non empty-membered FinSequenceSet of U
q11 is Relation-like NAT -defined U -valued Function-like non empty finite {} + 1 -element FinSequence-like FinSubsequence-like countable finite-support Element of ({} + 1) -tuples_on U
<*f*> ^ q11 is Relation-like NAT -defined U -valued Function-like non empty finite FinSequence-like FinSubsequence-like countable finite-support Element of U *
(U,q1) . (<*f*> ^ q11) is set
(U,q1) . q11 is set
q1 . (f,((U,q1) . q11)) is set
[f,((U,q1) . q11)] is non empty V15() set
q1 . [f,((U,q1) . q11)] is set
F is Element of U
<*F*> is Relation-like NAT -defined U -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like countable finite-support FinSequence of U
[1,F] is non empty V15() set
{[1,F]} is Relation-like Function-like constant non empty trivial finite 1 -element with_non-empty_elements non empty-membered countable finite-support set
(U,q1) . <*f*> is set
q1 . (((U,q1) . <*f*>),F) is set
[((U,q1) . <*f*>),F] is non empty V15() set
q1 . [((U,q1) . <*f*>),F] is set
q1 . (f,F) is Element of U
[f,F] is non empty V15() set
q1 . [f,F] is set
q11 is complex epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal ext-real non negative countable set
q11 + 1 is non empty complex epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal ext-real positive non negative countable set
(q11 + 1) -tuples_on U is functional non empty FinSequence-membered with_non-empty_elements non empty-membered FinSequenceSet of U
(q11 + 1) + 1 is non empty complex epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal ext-real positive non negative countable set
((q11 + 1) + 1) -tuples_on U is functional non empty FinSequence-membered with_non-empty_elements non empty-membered FinSequenceSet of U
F is Relation-like NAT -defined U -valued Function-like non empty finite (q11 + 1) + 1 -element FinSequence-like FinSubsequence-like countable finite-support Element of ((q11 + 1) + 1) -tuples_on U
<*f*> ^ F is Relation-like NAT -defined U -valued Function-like non empty finite FinSequence-like FinSubsequence-like countable finite-support Element of U *
(U,q1) . (<*f*> ^ F) is set
(U,q1) . F is set
q1 . (f,((U,q1) . F)) is set
[f,((U,q1) . F)] is non empty V15() set
q1 . [f,((U,q1) . F)] is set
(q11 + 1) + {} is non empty complex epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal ext-real positive non negative countable set
len F is non empty complex epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal ext-real positive non negative countable Element of NAT
F | (q11 + 1) is Relation-like NAT -defined U -valued Function-like finite FinSequence-like FinSubsequence-like countable finite-support FinSequence of U
Seg (q11 + 1) is non empty finite q11 + 1 -element q11 + 1 -element countable Element of bool NAT
q11 + 1 is non empty complex epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal ext-real positive non negative countable Element of NAT
{ b1 where b1 is complex epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal ext-real non negative countable Element of NAT : ( 1 <= b1 & b1 <= q11 + 1 ) } is set
F | (Seg (q11 + 1)) is Relation-like NAT -defined Seg (q11 + 1) -defined NAT -defined U -valued Function-like finite FinSequence-like FinSubsequence-like countable finite-support set
len (F | (q11 + 1)) is complex epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal ext-real non negative countable Element of NAT
p is Relation-like NAT -defined U -valued Function-like non empty finite q11 + 1 -element FinSequence-like FinSubsequence-like countable finite-support Element of (q11 + 1) -tuples_on U
F /. (len F) is Element of U
C is Relation-like NAT -defined U -valued Function-like non empty finite FinSequence-like FinSubsequence-like countable finite-support FinSequence of U
(U,q1) . C is set
y1 is Element of U
<*y1*> is Relation-like NAT -defined U -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like countable finite-support FinSequence of U
[1,y1] is non empty V15() set
{[1,y1]} is Relation-like Function-like constant non empty trivial finite 1 -element with_non-empty_elements non empty-membered countable finite-support set
(F | (q11 + 1)) ^ <*y1*> is Relation-like NAT -defined U -valued Function-like non empty finite FinSequence-like FinSubsequence-like countable finite-support Element of U *
<*f*> ^ ((F | (q11 + 1)) ^ <*y1*>) is Relation-like NAT -defined U -valued Function-like non empty finite FinSequence-like FinSubsequence-like countable finite-support Element of U *
(U,q1) . (<*f*> ^ ((F | (q11 + 1)) ^ <*y1*>)) is set
<*f*> ^ p is Relation-like NAT -defined U -valued Function-like non empty finite FinSequence-like FinSubsequence-like countable finite-support Element of U *
(<*f*> ^ p) ^ <*y1*> is Relation-like NAT -defined U -valued Function-like non empty finite FinSequence-like FinSubsequence-like countable finite-support Element of U *
(U,q1) . ((<*f*> ^ p) ^ <*y1*>) is set
(U,q1) . (<*f*> ^ p) is set
q1 . (((U,q1) . (<*f*> ^ p)),y1) is set
[((U,q1) . (<*f*> ^ p)),y1] is non empty V15() set
q1 . [((U,q1) . (<*f*> ^ p)),y1] is set
(U,q1) . p is set
q1 . (f,((U,q1) . p)) is set
[f,((U,q1) . p)] is non empty V15() set
q1 . [f,((U,q1) . p)] is set
q1 . ((q1 . (f,((U,q1) . p))),y1) is set
[(q1 . (f,((U,q1) . p))),y1] is non empty V15() set
q1 . [(q1 . (f,((U,q1) . p))),y1] is set
x is Element of U
q1 . (x,y1) is Element of U
[x,y1] is non empty V15() set
q1 . [x,y1] is set
q1 . (f,(q1 . (x,y1))) is Element of U
[f,(q1 . (x,y1))] is non empty V15() set
q1 . [f,(q1 . (x,y1))] is set
C ^ <*y1*> is Relation-like NAT -defined U -valued Function-like non empty finite FinSequence-like FinSubsequence-like countable finite-support Element of U *
(U,q1) . (C ^