:: FOMODEL0 semantic presentation

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

{ b

{} * 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

{ b

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

{ b

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

{ b

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

{ b

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

{ b

(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

{ b

(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

{ b

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

{ b

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

{ b

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

{ b

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

{ b

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

{ b

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

{ b

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

{ b

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

{ b

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 ^