REAL is V78() V79() V80() V84() V93() V94() V96() set
NAT is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite V41() V42() countable denumerable V78() V79() V80() V81() V82() V83() V84() V91() V93() Element of K32(REAL)
K32(REAL) is non empty set
2 is non empty epsilon-transitive epsilon-connected ordinal natural V28() V29() ext-real positive non negative finite V41() countable V65() V67() V78() V79() V80() V81() V82() V83() V91() V92() V93() V94() V95() Element of NAT
NAT is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite V41() V42() countable denumerable V78() V79() V80() V81() V82() V83() V84() V91() V93() set
K32(NAT) is non empty non trivial non finite set
K33(NAT,REAL) is Relation-like complex-valued ext-real-valued real-valued set
K32(K33(NAT,REAL)) is non empty set
K32(K32(REAL)) is non empty set
K32(NAT) is non empty non trivial non finite set
COMPLEX is V78() V84() set
RAT is V78() V79() V80() V81() V84() set
INT is V78() V79() V80() V81() V82() V84() set
{} is empty Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V28() V29() ext-real non positive non negative finite finite-yielding V40() V41() V43( {} ) Cardinal-yielding with_common_domain countable FinSequence-like FinSubsequence-like FinSequence-membered complex-valued ext-real-valued real-valued natural-valued V78() V79() V80() V81() V82() V83() V84() Function-yielding V90() V93() V94() V95() V96() V97() set
1 is non empty epsilon-transitive epsilon-connected ordinal natural V28() V29() ext-real positive non negative finite V41() countable V65() V67() V78() V79() V80() V81() V82() V83() V91() V92() V93() V94() V95() Element of NAT
{{},1} is non empty finite V40() countable V78() V79() V80() V81() V82() V83() V91() V92() V93() V94() V95() set
K542() is non empty set
0 is empty Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V28() V29() ext-real non positive non negative finite finite-yielding V40() V41() V43( {} ) Cardinal-yielding with_common_domain countable FinSequence-like FinSubsequence-like FinSequence-membered V65() V67() complex-valued ext-real-valued real-valued natural-valued V78() V79() V80() V81() V82() V83() V84() Function-yielding V90() V93() V94() V95() V96() V97() Element of NAT
{0,1} is non empty finite V40() countable V78() V79() V80() V81() V82() V83() V91() V92() V93() V94() V95() set
3 is non empty epsilon-transitive epsilon-connected ordinal natural V28() V29() ext-real positive non negative finite V41() countable V65() V67() V78() V79() V80() V81() V82() V83() V91() V92() V93() V94() V95() Element of NAT
dom {} is empty Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V28() V29() ext-real non positive non negative finite finite-yielding V40() V41() V43( {} ) Cardinal-yielding with_common_domain countable FinSequence-like FinSubsequence-like FinSequence-membered complex-valued ext-real-valued real-valued natural-valued V78() V79() V80() V81() V82() V83() V84() Function-yielding V90() V93() V94() V95() V96() V97() set
rng {} is empty trivial Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V28() V29() with_non-empty_elements ext-real non positive non negative finite finite-yielding V40() V41() V43( {} ) Cardinal-yielding with_common_domain countable FinSequence-like FinSubsequence-like FinSequence-membered complex-valued ext-real-valued real-valued natural-valued V72() decreasing non-decreasing non-increasing V78() V79() V80() V81() V82() V83() V84() Function-yielding V90() V93() V94() V95() V96() V97() set
Seg 1 is non empty trivial finite V43(1) countable V78() V79() V80() V81() V82() V83() V91() V92() V93() V94() V95() Element of K32(NAT)
{1} is non empty trivial finite V40() V43(1) countable V78() V79() V80() V81() V82() V83() V91() V92() V93() V94() V95() set
Seg 2 is non empty finite V43(2) countable V78() V79() V80() V81() V82() V83() V91() V92() V93() V94() V95() Element of K32(NAT)
{1,2} is non empty finite V40() countable V78() V79() V80() V81() V82() V83() V91() V92() V93() V94() V95() set
<:{}:> is Relation-like Function-like set
Frege {} is Relation-like Function-like set
{} .--> {} is non empty Relation-like {{}} -defined RAT -valued Function-like one-to-one finite Cardinal-yielding countable complex-valued ext-real-valued real-valued natural-valued Function-yielding V90() set
{{}} is non empty trivial functional finite V40() V43(1) with_common_domain countable V78() V79() V80() V81() V82() V83() V91() V92() V93() V94() V95() set
{{}} --> {} is non empty Relation-like {{}} -defined RAT -valued {{}} -valued Function-like constant total quasi_total finite Cardinal-yielding countable complex-valued ext-real-valued real-valued natural-valued Function-yielding V90() Element of K32(K33({{}},{{}}))
K33({{}},{{}}) is non empty Relation-like RAT -valued INT -valued finite countable complex-valued ext-real-valued real-valued natural-valued set
K32(K33({{}},{{}})) is non empty finite V40() countable set
{} * is non empty functional FinSequence-membered FinSequenceSet of {}
meet {} is set
len {} is empty Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V28() V29() ext-real non positive non negative finite finite-yielding V40() V41() V43( {} ) Cardinal-yielding with_common_domain countable FinSequence-like FinSubsequence-like FinSequence-membered complex-valued ext-real-valued real-valued natural-valued V78() V79() V80() V81() V82() V83() V84() Function-yielding V90() V93() V94() V95() V96() V97() set
0 ! is V28() V29() ext-real Element of REAL
i is set
j is set
<*i,j*> is non empty Relation-like NAT -defined Function-like finite V43(2) countable FinSequence-like FinSubsequence-like set
F is set
<*i,j*> +* (1,F) is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like set
<*F,j*> is non empty Relation-like NAT -defined Function-like finite V43(2) countable FinSequence-like FinSubsequence-like set
<*i,j*> +* (2,F) is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like set
<*i,F*> is non empty Relation-like NAT -defined Function-like finite V43(2) countable FinSequence-like FinSubsequence-like set
<*i,j*> . 1 is set
(<*i,j*> +* (2,F)) . 1 is set
<*i,j*> . 2 is set
(<*i,j*> +* (1,F)) . 2 is set
len <*i,j*> is non empty epsilon-transitive epsilon-connected ordinal natural V28() V29() ext-real positive non negative finite V41() countable V65() V67() V78() V79() V80() V81() V82() V83() V91() V92() V93() V94() V95() Element of NAT
dom <*i,j*> is non empty finite V43(2) countable V78() V79() V80() V81() V82() V83() V91() V92() V93() V94() V95() Element of K32(NAT)
(<*i,j*> +* (1,F)) . 1 is set
len (<*i,j*> +* (1,F)) is epsilon-transitive epsilon-connected ordinal natural V28() V29() ext-real non negative finite V41() countable V65() V67() V78() V79() V80() V81() V82() V83() V93() V94() V95() Element of NAT
(<*i,j*> +* (2,F)) . 2 is set
len (<*i,j*> +* (2,F)) is epsilon-transitive epsilon-connected ordinal natural V28() V29() ext-real non negative finite V41() countable V65() V67() V78() V79() V80() V81() V82() V83() V93() V94() V95() Element of NAT
i is set
j is set
F is set
g is set
F is Relation-like Function-like set
F +* (i,j) is Relation-like Function-like set
F +* (i,g) is Relation-like Function-like set
ii is Relation-like Function-like set
ii +* (i,F) is Relation-like Function-like set
ii +* (i,g) is Relation-like Function-like set
dom (ii +* (i,g)) is set
dom ii is set
dom (ii +* (i,F)) is set
dom (F +* (i,j)) is set
dom F is set
dom (F +* (i,g)) is set
k is set
(F +* (i,g)) . k is set
(ii +* (i,g)) . k is set
(F +* (i,g)) . k is set
F . k is set
(ii +* (i,F)) . k is set
ii . k is set
(ii +* (i,g)) . k is set
i is epsilon-transitive epsilon-connected ordinal natural V28() V29() ext-real non negative finite V41() countable V65() V67() V78() V79() V80() V81() V82() V83() V93() V94() V95() Element of NAT
j is set
F is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like set
F +* (i,j) is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like set
Del ((F +* (i,j)),i) is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like set
Del (F,i) is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like set
dom F is finite countable V78() V79() V80() V81() V82() V83() V93() V94() V95() Element of K32(NAT)
len F is epsilon-transitive epsilon-connected ordinal natural V28() V29() ext-real non negative finite V41() countable V65() V67() V78() V79() V80() V81() V82() V83() V93() V94() V95() Element of NAT
F is epsilon-transitive epsilon-connected ordinal natural V28() V29() ext-real non negative finite V41() countable set
F + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V28() V29() ext-real positive non negative finite V41() countable V65() V67() V78() V79() V80() V81() V82() V83() V91() V92() V93() V94() V95() Element of NAT
dom (F +* (i,j)) is finite countable V78() V79() V80() V81() V82() V83() V93() V94() V95() Element of K32(NAT)
len (F +* (i,j)) is epsilon-transitive epsilon-connected ordinal natural V28() V29() ext-real non negative finite V41() countable V65() V67() V78() V79() V80() V81() V82() V83() V93() V94() V95() Element of NAT
len (Del ((F +* (i,j)),i)) is epsilon-transitive epsilon-connected ordinal natural V28() V29() ext-real non negative finite V41() countable V65() V67() V78() V79() V80() V81() V82() V83() V93() V94() V95() Element of NAT
ii is epsilon-transitive epsilon-connected ordinal natural V28() V29() ext-real non negative finite V41() countable V65() V67() V78() V79() V80() V81() V82() V83() V93() V94() V95() Element of NAT
dom (Del ((F +* (i,j)),i)) is finite countable V78() V79() V80() V81() V82() V83() V93() V94() V95() Element of K32(NAT)
Seg ii is finite V43(ii) countable V78() V79() V80() V81() V82() V83() V93() V94() V95() Element of K32(NAT)
len (Del (F,i)) is epsilon-transitive epsilon-connected ordinal natural V28() V29() ext-real non negative finite V41() countable V65() V67() V78() V79() V80() V81() V82() V83() V93() V94() V95() Element of NAT
k is epsilon-transitive epsilon-connected ordinal natural V28() V29() ext-real non negative finite V41() countable set
(Del ((F +* (i,j)),i)) . k is set
(F +* (i,j)) . k is set
F . k is set
(Del (F,i)) . k is set
k + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V28() V29() ext-real positive non negative finite V41() countable V65() V67() V78() V79() V80() V81() V82() V83() V91() V92() V93() V94() V95() Element of NAT
(Del ((F +* (i,j)),i)) . k is set
(F +* (i,j)) . (k + 1) is set
F . (k + 1) is set
(Del (F,i)) . k is set
dom F is finite countable V78() V79() V80() V81() V82() V83() V93() V94() V95() Element of K32(NAT)
dom F is finite countable V78() V79() V80() V81() V82() V83() V93() V94() V95() Element of K32(NAT)
i is epsilon-transitive epsilon-connected ordinal natural V28() V29() ext-real non negative finite V41() countable V65() V67() V78() V79() V80() V81() V82() V83() V93() V94() V95() Element of NAT
j is set
F is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like set
F +* (i,j) is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like set
Del (F,i) is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like set
g is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like set
g +* (i,j) is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like set
Del (g,i) is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like set
dom (F +* (i,j)) is finite countable V78() V79() V80() V81() V82() V83() V93() V94() V95() Element of K32(NAT)
dom F is finite countable V78() V79() V80() V81() V82() V83() V93() V94() V95() Element of K32(NAT)
dom (g +* (i,j)) is finite countable V78() V79() V80() V81() V82() V83() V93() V94() V95() Element of K32(NAT)
dom g is finite countable V78() V79() V80() V81() V82() V83() V93() V94() V95() Element of K32(NAT)
len g is epsilon-transitive epsilon-connected ordinal natural V28() V29() ext-real non negative finite V41() countable V65() V67() V78() V79() V80() V81() V82() V83() V93() V94() V95() Element of NAT
Seg (len g) is finite V43( len g) countable V78() V79() V80() V81() V82() V83() V93() V94() V95() Element of K32(NAT)
len F is epsilon-transitive epsilon-connected ordinal natural V28() V29() ext-real non negative finite V41() countable V65() V67() V78() V79() V80() V81() V82() V83() V93() V94() V95() Element of NAT
Seg (len F) is finite V43( len F) countable V78() V79() V80() V81() V82() V83() V93() V94() V95() Element of K32(NAT)
dom (Del (F,i)) is finite countable V78() V79() V80() V81() V82() V83() V93() V94() V95() Element of K32(NAT)
len (Del (F,i)) is epsilon-transitive epsilon-connected ordinal natural V28() V29() ext-real non negative finite V41() countable V65() V67() V78() V79() V80() V81() V82() V83() V93() V94() V95() Element of NAT
Seg (len (Del (F,i))) is finite V43( len (Del (F,i))) countable V78() V79() V80() V81() V82() V83() V93() V94() V95() Element of K32(NAT)
k1 is epsilon-transitive epsilon-connected ordinal natural V28() V29() ext-real non negative finite V41() countable set
k1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V28() V29() ext-real positive non negative finite V41() countable V65() V67() V78() V79() V80() V81() V82() V83() V91() V92() V93() V94() V95() Element of NAT
k is epsilon-transitive epsilon-connected ordinal natural V28() V29() ext-real non negative finite V41() countable V65() V67() V78() V79() V80() V81() V82() V83() V93() V94() V95() Element of NAT
len (Del (g,i)) is epsilon-transitive epsilon-connected ordinal natural V28() V29() ext-real non negative finite V41() countable V65() V67() V78() V79() V80() V81() V82() V83() V93() V94() V95() Element of NAT
k is epsilon-transitive epsilon-connected ordinal natural V28() V29() ext-real non negative finite V41() countable set
(Del (F,i)) . k is set
F . k is set
(g +* (i,j)) . k is set
g . k is set
(Del (g,i)) . k is set
k + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V28() V29() ext-real positive non negative finite V41() countable V65() V67() V78() V79() V80() V81() V82() V83() V91() V92() V93() V94() V95() Element of NAT
(Del (F,i)) . k is set
F . (k + 1) is set
(g +* (i,j)) . (k + 1) is set
g . (k + 1) is set
(Del (g,i)) . k is set
i is set
0 -tuples_on i is functional with_common_domain product-like FinSequence-membered FinSequenceSet of i
i * is non empty functional FinSequence-membered FinSequenceSet of i
{ b1 where b1 is Relation-like NAT -defined i -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of i * : len b1 = 0 } is set
F is set
g is Relation-like NAT -defined i -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of i *
len g is epsilon-transitive epsilon-connected ordinal natural V28() V29() ext-real non negative finite V41() countable V65() V67() V78() V79() V80() V81() V82() V83() V93() V94() V95() Element of NAT
<*> (i *) is empty proper Relation-like non-empty empty-yielding NAT -defined i * -valued Function-like one-to-one constant functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V28() V29() ext-real non positive non negative finite finite-yielding V40() V41() V43( {} ) Cardinal-yielding with_common_domain countable FinSequence-like FinSubsequence-like FinSequence-membered complex-valued ext-real-valued real-valued natural-valued V78() V79() V80() V81() V82() V83() V84() Function-yielding V90() V93() V94() V95() V96() V97() FinSequence of i *
K33(NAT,(i *)) is non empty non trivial Relation-like non finite set
i is epsilon-transitive epsilon-connected ordinal natural V28() V29() ext-real non negative finite V41() countable V65() V67() V78() V79() V80() V81() V82() V83() V93() V94() V95() Element of NAT
i -tuples_on {} is functional finite with_common_domain product-like countable FinSequence-membered FinSequenceSet of {}
{ b1 where b1 is Relation-like NAT -defined {} -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of {} * : len b1 = i } is set
j is set
F is empty Relation-like non-empty empty-yielding NAT -defined {} -valued Function-like one-to-one constant functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V28() V29() ext-real non positive non negative finite finite-yielding V40() V41() V43( {} ) Cardinal-yielding with_common_domain countable FinSequence-like FinSubsequence-like FinSequence-membered complex-valued ext-real-valued real-valued natural-valued V78() V79() V80() V81() V82() V83() V84() Function-yielding V90() V93() V94() V95() V96() V97() Element of {} *
len F is empty Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V28() V29() ext-real non positive non negative finite finite-yielding V40() V41() V43( {} ) Cardinal-yielding with_common_domain countable FinSequence-like FinSubsequence-like FinSequence-membered V65() V67() complex-valued ext-real-valued real-valued natural-valued V78() V79() V80() V81() V82() V83() V84() Function-yielding V90() V93() V94() V95() V96() V97() Element of NAT
i is Relation-like Function-like set
rng i is set
<:i:> is Relation-like Function-like set
dom <:i:> is set
doms i is Relation-like Function-like set
meet (doms i) is set
rng (doms i) is set
meet (rng (doms i)) is set
dom i is set
j is set
i . j is set
dom (doms i) is set
SubFuncs (rng i) is set
i " (SubFuncs (rng i)) is set
(doms i) . j is set
i is non empty set
1 -tuples_on i is non empty functional with_common_domain product-like FinSequence-membered FinSequenceSet of i
i * is non empty functional FinSequence-membered FinSequenceSet of i
{ b1 where b1 is Relation-like NAT -defined i -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of i * : len b1 = 1 } is set
j is Relation-like Function-like set
rng j is set
<*j*> is non empty trivial Relation-like NAT -defined Function-like constant finite V43(1) countable FinSequence-like FinSubsequence-like Function-yielding V90() V97() set
<:<*j*>:> is Relation-like Function-like set
rng <:<*j*>:> is set
dom <:<*j*>:> is set
dom j is set
g is set
F is set
<:<*j*>:> . F is set
j . F is set
ii is Element of i
<*ii*> is non empty trivial Relation-like NAT -defined i -valued Function-like constant finite V43(1) countable FinSequence-like FinSubsequence-like FinSequence of i
<*(j . F)*> is non empty trivial Relation-like NAT -defined Function-like constant finite V43(1) countable FinSequence-like FinSubsequence-like set
F is Element of i
<*F*> is non empty trivial Relation-like NAT -defined i -valued Function-like constant finite V43(1) countable FinSequence-like FinSubsequence-like FinSequence of i
ii is set
j . ii is set
<:<*j*>:> . ii is set
i is epsilon-transitive epsilon-connected ordinal natural V28() V29() ext-real non negative finite V41() countable V65() V67() V78() V79() V80() V81() V82() V83() V93() V94() V95() Element of NAT
j is epsilon-transitive epsilon-connected ordinal natural V28() V29() ext-real non negative finite V41() countable V65() V67() V78() V79() V80() V81() V82() V83() V93() V94() V95() Element of NAT
j + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V28() V29() ext-real positive non negative finite V41() countable V65() V67() V78() V79() V80() V81() V82() V83() V91() V92() V93() V94() V95() Element of NAT
F is non empty set
(j + 1) -tuples_on F is non empty functional with_common_domain product-like FinSequence-membered FinSequenceSet of F
F * is non empty functional FinSequence-membered FinSequenceSet of F
{ b1 where b1 is Relation-like NAT -defined F -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of F * : len b1 = j + 1 } is set
j -tuples_on F is non empty functional with_common_domain product-like FinSequence-membered FinSequenceSet of F
{ b1 where b1 is Relation-like NAT -defined F -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of F * : len b1 = j } is set
F is Relation-like NAT -defined F -valued Function-like finite V43(j + 1) countable FinSequence-like FinSubsequence-like Element of (j + 1) -tuples_on F
Del (F,i) is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like set
len F is epsilon-transitive epsilon-connected ordinal natural V28() V29() ext-real non negative finite V41() countable V65() V67() V78() V79() V80() V81() V82() V83() V93() V94() V95() Element of NAT
dom F is finite V43(j + 1) countable V78() V79() V80() V81() V82() V83() V93() V94() V95() Element of K32(NAT)
len (Del (F,i)) is epsilon-transitive epsilon-connected ordinal natural V28() V29() ext-real non negative finite V41() countable V65() V67() V78() V79() V80() V81() V82() V83() V93() V94() V95() Element of NAT
i is set
i * is non empty functional FinSequence-membered FinSequenceSet of i
j is functional FinSequence-membered FinSequenceSet of i
F is set
j is Relation-like Function-like set
F is Relation-like Function-like set
i is functional () set
union i is set
j is set
F is set
[j,F] is set
{j,F} is non empty finite countable set
{j} is non empty trivial finite V43(1) countable set
{{j,F},{j}} is non empty finite V40() countable set
g is set
[j,g] is set
{j,g} is non empty finite countable set
{{j,g},{j}} is non empty finite V40() countable set
F is set
ii is set
k is Relation-like Function-like set
dom k is set
k . j is set
k is Relation-like Function-like set
dom k is set
k . j is set
(dom k) /\ (dom k) is set
j is set
F is set
i is set
union i is set
j is set
F is set
g is set
[F,g] is set
{F,g} is non empty finite countable set
{F} is non empty trivial finite V43(1) countable set
{{F,g},{F}} is non empty finite V40() countable set
F is set
[F,F] is set
{F,F} is non empty finite countable set
{{F,F},{F}} is non empty finite V40() countable set
F is set
j is Relation-like Function-like set
F is Relation-like Function-like set
g is set
dom j is set
dom F is set
(dom j) /\ (dom F) is set
j . g is set
F . g is set
F is set
[g,F] is set
{g,F} is non empty finite countable set
{g} is non empty trivial finite V43(1) countable set
{{g,F},{g}} is non empty finite V40() countable set
ii is set
[g,ii] is set
{g,ii} is non empty finite countable set
{{g,ii},{g}} is non empty finite V40() countable set
i is set
j is set
g is Relation-like Function-like set
F is Relation-like Function-like set
g is Relation-like Function-like epsilon-transitive epsilon-connected ordinal natural V28() V29() ext-real non negative finite V41() countable V65() V67() Element of {{}}
K33(i,j) is Relation-like set
K32(K33(i,j)) is non empty set
i is non empty functional () set
union i is Relation-like Function-like set
dom (union i) is set
{ (dom b1) where b1 is Relation-like Function-like Element of i : verum } is set
union { (dom b1) where b1 is Relation-like Function-like Element of i : verum } is set
F is set
g is set
[F,g] is set
{F,g} is non empty finite countable set
{F} is non empty trivial finite V43(1) countable set
{{F,g},{F}} is non empty finite V40() countable set
F is set
ii is Relation-like Function-like Element of i
dom ii is set
g is set
F is Relation-like Function-like Element of i
dom F is set
ii is set
[F,ii] is set
{F,ii} is non empty finite countable set
{{F,ii},{F}} is non empty finite V40() countable set
i is functional () set
union i is Relation-like Function-like set
dom (union i) is set
j is Relation-like Function-like set
dom j is set
F is set
g is set
[F,g] is set
{F,g} is non empty finite countable set
{F} is non empty trivial finite V43(1) countable set
{{F,g},{F}} is non empty finite V40() countable set
F is set
(union i) . F is set
j . F is set
g is set
[F,g] is set
{F,g} is non empty finite countable set
{F} is non empty trivial finite V43(1) countable set
{{F,g},{F}} is non empty finite V40() countable set
i is non empty functional () set
union i is Relation-like Function-like set
rng (union i) is set
{ (rng b1) where b1 is Relation-like Function-like Element of i : verum } is set
union { (rng b1) where b1 is Relation-like Function-like Element of i : verum } is set
F is set
g is set
[g,F] is set
{g,F} is non empty finite countable set
{g} is non empty trivial finite V43(1) countable set
{{g,F},{g}} is non empty finite V40() countable set
F is set
ii is Relation-like Function-like Element of i
rng ii is set
g is set
F is Relation-like Function-like Element of i
rng F is set
ii is set
[ii,F] is set
{ii,F} is non empty finite countable set
{ii} is non empty trivial finite V43(1) countable set
{{ii,F},{ii}} is non empty finite V40() countable set
i is set
j is set
F is non empty PartFunc-set of i,j
g is set
i is set
j is set
K33(i,j) is Relation-like set
K32(K33(i,j)) is non empty set
F is non empty functional () PartFunc-set of i,j
union F is Relation-like Function-like set
{ (dom b1) where b1 is Relation-like i -defined j -valued Function-like Element of F : verum } is set
{ (rng b1) where b1 is Relation-like i -defined j -valued Function-like Element of F : verum } is set
ii is Relation-like Function-like set
rng ii is set
k is set
union { (rng b1) where b1 is Relation-like i -defined j -valued Function-like Element of F : verum } is set
k is set
ij is Relation-like i -defined j -valued Function-like Element of F
rng ij is set
dom ii is set
k is set
union { (dom b1) where b1 is Relation-like i -defined j -valued Function-like Element of F : verum } is set
k is set
ij is Relation-like i -defined j -valued Function-like Element of F
dom ij is Element of K32(i)
K32(i) is non empty set
NAT * is non empty functional FinSequence-membered FinSequenceSet of NAT
i is empty Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V28() V29() ext-real non positive non negative finite finite-yielding V40() V41() V43( {} ) Cardinal-yielding with_common_domain countable FinSequence-like FinSubsequence-like FinSequence-membered complex-valued ext-real-valued real-valued natural-valued V78() V79() V80() V81() V82() V83() V84() Function-yielding V90() V93() V94() V95() V96() V97() set
dom i is empty proper Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V28() V29() ext-real non positive non negative finite finite-yielding V40() V41() V43( {} ) Cardinal-yielding with_common_domain countable FinSequence-like FinSubsequence-like FinSequence-membered complex-valued ext-real-valued real-valued natural-valued V78() V79() V80() V81() V82() V83() V84() Function-yielding V90() V93() V94() V95() V96() V97() Element of K32(NAT)
i is epsilon-transitive epsilon-connected ordinal natural V28() V29() ext-real non negative finite V41() countable V65() V67() V78() V79() V80() V81() V82() V83() V93() V94() V95() Element of NAT
j is non empty set
i -tuples_on j is non empty functional with_common_domain product-like FinSequence-membered FinSequenceSet of j
j * is non empty functional FinSequence-membered FinSequenceSet of j
{ b1 where b1 is Relation-like NAT -defined j -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of j * : len b1 = i } is set
F is Relation-like set
dom F is set
i is Relation-like set
dom i is set
i is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like set
j is set
i .--> j is non empty Relation-like {i} -defined Function-like one-to-one finite countable set
{i} is non empty trivial functional finite V40() V43(1) with_common_domain countable set
{i} --> j is non empty Relation-like {i} -defined {j} -valued Function-like constant total quasi_total finite countable Element of K32(K33({i},{j}))
{j} is non empty trivial finite V43(1) countable set
K33({i},{j}) is non empty Relation-like finite countable set
K32(K33({i},{j})) is non empty finite V40() countable set
dom (i .--> j) is non empty trivial functional finite V40() V43(1) with_common_domain countable Element of K32({i})
K32({i}) is non empty finite V40() countable set
the Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like set is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like set
the Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like set .--> 0 is non empty Relation-like { the Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like set } -defined NAT -valued RAT -valued INT -valued Function-like one-to-one finite Cardinal-yielding countable complex-valued ext-real-valued real-valued natural-valued Function-yielding V90() homogeneous set
{ the Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like set } is non empty trivial functional finite V40() V43(1) with_common_domain countable set
{ the Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like set } --> 0 is non empty Relation-like { the Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like set } -defined NAT -valued RAT -valued INT -valued {0} -valued Function-like constant total quasi_total finite Cardinal-yielding countable complex-valued ext-real-valued real-valued natural-valued Function-yielding V90() Element of K32(K33({ the Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like set },{0}))
{0} is non empty trivial functional finite V40() V43(1) with_common_domain countable V78() V79() V80() V81() V82() V83() V91() V92() V93() V94() V95() set
K33({ the Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like set },{0}) is non empty Relation-like RAT -valued INT -valued finite countable complex-valued ext-real-valued real-valued natural-valued set
K32(K33({ the Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like set },{0})) is non empty finite V40() countable set
i is Relation-like Function-like homogeneous set
j is Relation-like Function-like set
i * j is Relation-like Function-like set
dom (i * j) is set
dom i is with_common_domain set
i is set
i * is non empty functional FinSequence-membered FinSequenceSet of i
j is set
K33((i *),j) is Relation-like set
K32(K33((i *),j)) is non empty set
g is Relation-like i * -defined j -valued Function-like Element of K32(K33((i *),j))
dom g is functional FinSequence-membered Element of K32((i *))
K32((i *)) is non empty set
i is non empty set
i * is non empty functional FinSequence-membered FinSequenceSet of i
j is non empty set
K33((i *),j) is non empty Relation-like set
K32(K33((i *),j)) is non empty set
the Element of j is Element of j
K32((i *)) is non empty set
0 -tuples_on i is non empty functional with_common_domain product-like FinSequence-membered FinSequenceSet of i
{ b1 where b1 is Relation-like NAT -defined i -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of i * : len b1 = 0 } is set
g is non empty functional FinSequence-membered Element of K32((i *))
g --> the Element of j is non empty Relation-like i * -defined g -defined j -valued Function-like constant total Element of PFuncs ((i *),j)
PFuncs ((i *),j) is non empty functional PartFunc-set of i * ,j
{ the Element of j} is non empty trivial finite V43(1) countable set
K33(g,{ the Element of j}) is non empty Relation-like set
F is Relation-like i * -defined j -valued Function-like Element of K32(K33((i *),j))
dom F is functional FinSequence-membered Element of K32((i *))
i is non empty set
i * is non empty functional FinSequence-membered FinSequenceSet of i
K33((i *),i) is non empty Relation-like set
K32(K33((i *),i)) is non empty set
the epsilon-transitive epsilon-connected ordinal natural V28() V29() ext-real non negative finite V41() countable V65() V67() V78() V79() V80() V81() V82() V83() V93() V94() V95() Element of NAT is epsilon-transitive epsilon-connected ordinal natural V28() V29() ext-real non negative finite V41() countable V65() V67() V78() V79() V80() V81() V82() V83() V93() V94() V95() Element of NAT
the Element of i is Element of i
K32((i *)) is non empty set
the epsilon-transitive epsilon-connected ordinal natural V28() V29() ext-real non negative finite V41() countable V65() V67() V78() V79() V80() V81() V82() V83() V93() V94() V95() Element of NAT -tuples_on i is non empty functional with_common_domain product-like FinSequence-membered FinSequenceSet of i
{ b1 where b1 is Relation-like NAT -defined i -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of i * : len b1 = the epsilon-transitive epsilon-connected ordinal natural V28() V29() ext-real non negative finite V41() countable V65() V67() V78() V79() V80() V81() V82() V83() V93() V94() V95() Element of NAT } is set
g is non empty functional FinSequence-membered Element of K32((i *))
g --> the Element of i is non empty Relation-like i * -defined g -defined i -valued Function-like constant total Element of PFuncs ((i *),i)
PFuncs ((i *),i) is non empty functional PartFunc-set of i * ,i
{ the Element of i} is non empty trivial finite V43(1) countable set
K33(g,{ the Element of i}) is non empty Relation-like set
F is Relation-like i * -defined i -valued Function-like Element of K32(K33((i *),i))
dom F is functional FinSequence-membered Element of K32((i *))
ii is Relation-like NAT -defined i -valued Function-like finite countable FinSequence-like FinSubsequence-like FinSequence of i
len ii is epsilon-transitive epsilon-connected ordinal natural V28() V29() ext-real non negative finite V41() countable V65() V67() V78() V79() V80() V81() V82() V83() V93() V94() V95() Element of NAT
k is Relation-like NAT -defined i -valued Function-like finite countable FinSequence-like FinSubsequence-like FinSequence of i
len k is epsilon-transitive epsilon-connected ordinal natural V28() V29() ext-real non negative finite V41() countable V65() V67() V78() V79() V80() V81() V82() V83() V93() V94() V95() Element of NAT
dom F is functional FinSequence-membered set
K32((NAT *)) is non empty set
0 -tuples_on NAT is non empty functional with_common_domain product-like FinSequence-membered FinSequenceSet of NAT
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of NAT * : len b1 = 0 } is set
i is non empty functional FinSequence-membered Element of K32((NAT *))
i --> 0 is non empty Relation-like NAT * -defined i -defined NAT -valued RAT -valued INT -valued Function-like constant total Cardinal-yielding complex-valued ext-real-valued real-valued natural-valued Function-yielding V90() Element of PFuncs ((NAT *),NAT)
PFuncs ((NAT *),NAT) is non empty functional PartFunc-set of NAT * , NAT
{0} is non empty trivial functional finite V40() V43(1) with_common_domain countable V78() V79() V80() V81() V82() V83() V91() V92() V93() V94() V95() set
K33(i,{0}) is non empty Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set
dom (i --> 0) is non empty functional FinSequence-membered Element of K32(i)
K32(i) is non empty set
F is Relation-like NAT * -defined Function-like set
g is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued FinSequence of NAT
len g is epsilon-transitive epsilon-connected ordinal natural V28() V29() ext-real non negative finite V41() countable V65() V67() V78() V79() V80() V81() V82() V83() V93() V94() V95() Element of NAT
F is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued FinSequence of NAT
len F is epsilon-transitive epsilon-connected ordinal natural V28() V29() ext-real non negative finite V41() countable V65() V67() V78() V79() V80() V81() V82() V83() V93() V94() V95() Element of NAT
dom F is functional FinSequence-membered Element of K32((NAT *))
(len F) -tuples_on NAT is non empty functional with_common_domain product-like FinSequence-membered FinSequenceSet of NAT
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of NAT * : len b1 = len F } is set
dom F is functional FinSequence-membered Element of K32((NAT *))
K33((NAT *),NAT) is non empty non trivial Relation-like RAT -valued INT -valued non finite complex-valued ext-real-valued real-valued natural-valued set
K32(K33((NAT *),NAT)) is non empty non trivial non finite set
i is Relation-like NAT * -defined NAT -valued Function-like complex-valued ext-real-valued real-valued natural-valued Element of K32(K33((NAT *),NAT))
j is Relation-like NAT * -defined NAT -valued Function-like complex-valued ext-real-valued real-valued natural-valued Element of K32(K33((NAT *),NAT))
i is Relation-like NAT * -defined NAT -valued Function-like complex-valued ext-real-valued real-valued natural-valued Element of K32(K33((NAT *),NAT))
j is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued FinSequence of NAT
len j is epsilon-transitive epsilon-connected ordinal natural V28() V29() ext-real non negative finite V41() countable V65() V67() V78() V79() V80() V81() V82() V83() V93() V94() V95() Element of NAT
F is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued FinSequence of NAT
len F is epsilon-transitive epsilon-connected ordinal natural V28() V29() ext-real non negative finite V41() countable V65() V67() V78() V79() V80() V81() V82() V83() V93() V94() V95() Element of NAT
dom i is functional FinSequence-membered Element of K32((NAT *))
K32((NAT *)) is non empty set
i is Relation-like NAT * -defined RAT -valued Function-like complex-valued ext-real-valued real-valued natural-valued () set
rng i is V78() V79() V80() V81() V82() V83() V93() set
dom i is functional FinSequence-membered Element of K32((NAT *))
K32((NAT *)) is non empty set
F is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued FinSequence of NAT
len F is epsilon-transitive epsilon-connected ordinal natural V28() V29() ext-real non negative finite V41() countable V65() V67() V78() V79() V80() V81() V82() V83() V93() V94() V95() Element of NAT
g is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued FinSequence of NAT
len g is epsilon-transitive epsilon-connected ordinal natural V28() V29() ext-real non negative finite V41() countable V65() V67() V78() V79() V80() V81() V82() V83() V93() V94() V95() Element of NAT
j is Relation-like NAT * -defined NAT -valued Function-like complex-valued ext-real-valued real-valued natural-valued Element of K32(K33((NAT *),NAT))
arity {} is epsilon-transitive epsilon-connected ordinal natural V28() V29() ext-real non negative finite V41() countable V65() V67() V78() V79() V80() V81() V82() V83() V93() V94() V95() Element of NAT
dom {} is empty proper Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V28() V29() ext-real non positive non negative finite finite-yielding V40() V41() V43( {} ) Cardinal-yielding with_common_domain countable FinSequence-like FinSubsequence-like FinSequence-membered complex-valued ext-real-valued real-valued natural-valued V78() V79() V80() V81() V82() V83() V84() Function-yielding V90() V93() V94() V95() V96() V97() homogeneous Element of K32(NAT)
i is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like set
i is Relation-like homogeneous set
dom i is with_common_domain set
arity i is epsilon-transitive epsilon-connected ordinal natural V28() V29() ext-real non negative finite V41() countable set
i is set
i * is non empty functional FinSequence-membered FinSequenceSet of i
j is set
K33((i *),j) is Relation-like set
K32(K33((i *),j)) is non empty set
F is Relation-like i * -defined j -valued Function-like homogeneous Element of K32(K33((i *),j))
dom F is functional with_common_domain FinSequence-membered Element of K32((i *))
K32((i *)) is non empty set
arity F is epsilon-transitive epsilon-connected ordinal natural V28() V29() ext-real non negative finite V41() countable V65() V67() V78() V79() V80() V81() V82() V83() V93() V94() V95() Element of NAT
(arity F) -tuples_on i is functional with_common_domain product-like FinSequence-membered FinSequenceSet of i
{ b1 where b1 is Relation-like NAT -defined i -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of i * : len b1 = arity F } is set
g is set
<*> (i *) is empty proper Relation-like non-empty empty-yielding NAT -defined i * -valued Function-like one-to-one constant functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V28() V29() ext-real non positive non negative finite finite-yielding V40() V41() V43( {} ) Cardinal-yielding with_common_domain countable FinSequence-like FinSubsequence-like FinSequence-membered complex-valued ext-real-valued real-valued natural-valued V78() V79() V80() V81() V82() V83() V84() Function-yielding V90() V93() V94() V95() V96() V97() homogeneous FinSequence of i *
K33(NAT,(i *)) is non empty non trivial Relation-like non finite set
len (<*> (i *)) is empty Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V28() V29() ext-real non positive non negative finite finite-yielding V40() V41() V43( {} ) Cardinal-yielding with_common_domain countable FinSequence-like FinSubsequence-like FinSequence-membered V65() V67() complex-valued ext-real-valued real-valued natural-valued V78() V79() V80() V81() V82() V83() V84() Function-yielding V90() V93() V94() V95() V96() V97() homogeneous Element of NAT
0 -tuples_on i is functional with_common_domain product-like FinSequence-membered FinSequenceSet of i
{ b1 where b1 is Relation-like NAT -defined i -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of i * : len b1 = 0 } is set
F is non empty set
ii is Relation-like NAT -defined F -valued Function-like finite countable FinSequence-like FinSubsequence-like FinSequence of F
len ii is epsilon-transitive epsilon-connected ordinal natural V28() V29() ext-real non negative finite V41() countable V65() V67() V78() V79() V80() V81() V82() V83() V93() V94() V95() Element of NAT
(arity F) -tuples_on F is non empty functional with_common_domain product-like FinSequence-membered FinSequenceSet of F
F * is non empty functional FinSequence-membered FinSequenceSet of F
{ b1 where b1 is Relation-like NAT -defined F -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of F * : len b1 = arity F } is set
i is Relation-like NAT * -defined Function-like homogeneous set
dom i is functional with_common_domain FinSequence-membered Element of K32((NAT *))
K32((NAT *)) is non empty set
arity i is epsilon-transitive epsilon-connected ordinal natural V28() V29() ext-real non negative finite V41() countable V65() V67() V78() V79() V80() V81() V82() V83() V93() V94() V95() Element of NAT
(arity i) -tuples_on NAT is non empty functional with_common_domain product-like FinSequence-membered FinSequenceSet of NAT
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of NAT * : len b1 = arity i } is set
j is set
F is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued FinSequence of NAT
len F is epsilon-transitive epsilon-connected ordinal natural V28() V29() ext-real non negative finite V41() countable V65() V67() V78() V79() V80() V81() V82() V83() V93() V94() V95() Element of NAT
i is non empty set
i * is non empty functional FinSequence-membered FinSequenceSet of i
K33((i *),i) is non empty Relation-like set
K32(K33((i *),i)) is non empty set
F is Relation-like i * -defined i -valued Function-like homogeneous Element of K32(K33((i *),i))
dom F is functional with_common_domain FinSequence-membered Element of K32((i *))
K32((i *)) is non empty set
arity F is epsilon-transitive epsilon-connected ordinal natural V28() V29() ext-real non negative finite V41() countable V65() V67() V78() V79() V80() V81() V82() V83() V93() V94() V95() Element of NAT
(arity F) -tuples_on i is non empty functional with_common_domain product-like FinSequence-membered FinSequenceSet of i
{ b1 where b1 is Relation-like NAT -defined i -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of i * : len b1 = arity F } is set
g is non empty Relation-like i * -defined i -valued Function-like homogeneous quasi_total Element of K32(K33((i *),i))
dom g is non empty functional with_common_domain FinSequence-membered Element of K32((i *))
F is set
ii is Relation-like NAT -defined i -valued Function-like finite countable FinSequence-like FinSubsequence-like FinSequence of i
len ii is epsilon-transitive epsilon-connected ordinal natural V28() V29() ext-real non negative finite V41() countable V65() V67() V78() V79() V80() V81() V82() V83() V93() V94() V95() Element of NAT
k is set
k is Relation-like NAT -defined i -valued Function-like finite V43( arity F) countable FinSequence-like FinSubsequence-like Element of (arity F) -tuples_on i
len k is epsilon-transitive epsilon-connected ordinal natural V28() V29() ext-real non negative finite V41() countable V65() V67() V78() V79() V80() V81() V82() V83() V93() V94() V95() Element of NAT
g is Relation-like NAT -defined i -valued Function-like finite countable FinSequence-like FinSubsequence-like FinSequence of i
len g is epsilon-transitive epsilon-connected ordinal natural V28() V29() ext-real non negative finite V41() countable V65() V67() V78() V79() V80() V81() V82() V83() V93() V94() V95() Element of NAT
F is Relation-like NAT -defined i -valued Function-like finite countable FinSequence-like FinSubsequence-like FinSequence of i
len F is epsilon-transitive epsilon-connected ordinal natural V28() V29() ext-real non negative finite V41() countable V65() V67() V78() V79() V80() V81() V82() V83() V93() V94() V95() Element of NAT
dom F is functional with_common_domain FinSequence-membered set
i is set
i * is non empty functional FinSequence-membered FinSequenceSet of i
K33((i *),i) is Relation-like set
K32(K33((i *),i)) is non empty set
j is Relation-like i * -defined i -valued Function-like homogeneous Element of K32(K33((i *),i))
dom j is functional with_common_domain FinSequence-membered Element of K32((i *))
K32((i *)) is non empty set
arity j is epsilon-transitive epsilon-connected ordinal natural V28() V29() ext-real non negative finite V41() countable V65() V67() V78() V79() V80() V81() V82() V83() V93() V94() V95() Element of NAT
(arity j) -tuples_on i is functional with_common_domain product-like FinSequence-membered FinSequenceSet of i
{ b1 where b1 is Relation-like NAT -defined i -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of i * : len b1 = arity j } is set
i is Relation-like NAT * -defined RAT -valued Function-like complex-valued ext-real-valued real-valued natural-valued homogeneous set
dom i is functional with_common_domain FinSequence-membered Element of K32((NAT *))
K32((NAT *)) is non empty set
arity i is epsilon-transitive epsilon-connected ordinal natural V28() V29() ext-real non negative finite V41() countable V65() V67() V78() V79() V80() V81() V82() V83() V93() V94() V95() Element of NAT
(arity i) -tuples_on NAT is non empty functional with_common_domain product-like FinSequence-membered FinSequenceSet of NAT
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of NAT * : len b1 = arity i } is set
j is non empty Relation-like NAT * -defined NAT -valued Function-like complex-valued ext-real-valued real-valued natural-valued homogeneous quasi_total () Element of K32(K33((NAT *),NAT))
dom j is non empty functional with_common_domain FinSequence-membered Element of K32((NAT *))
F is set
g is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued FinSequence of NAT
len g is epsilon-transitive epsilon-connected ordinal natural V28() V29() ext-real non negative finite V41() countable V65() V67() V78() V79() V80() V81() V82() V83() V93() V94() V95() Element of NAT
F is set
ii is Relation-like NAT -defined NAT -valued Function-like finite V43( arity i) countable FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued Element of (arity i) -tuples_on NAT
len ii is epsilon-transitive epsilon-connected ordinal natural V28() V29() ext-real non negative finite V41() countable V65() V67() V78() V79() V80() V81() V82() V83() V93() V94() V95() Element of NAT
j is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued FinSequence of NAT
len j is epsilon-transitive epsilon-connected ordinal natural V28() V29() ext-real non negative finite V41() countable V65() V67() V78() V79() V80() V81() V82() V83() V93() V94() V95() Element of NAT
F is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued FinSequence of NAT
len F is epsilon-transitive epsilon-connected ordinal natural V28() V29() ext-real non negative finite V41() countable V65() V67() V78() V79() V80() V81() V82() V83() V93() V94() V95() Element of NAT
i is non empty set
i * is non empty functional FinSequence-membered FinSequenceSet of i
K33((i *),i) is non empty Relation-like set
K32(K33((i *),i)) is non empty set
j is non empty Relation-like i * -defined i -valued Function-like homogeneous Element of K32(K33((i *),i))
dom j is non empty functional with_common_domain FinSequence-membered Element of K32((i *))
K32((i *)) is non empty set
arity j is epsilon-transitive epsilon-connected ordinal natural V28() V29() ext-real non negative finite V41() countable V65() V67() V78() V79() V80() V81() V82() V83() V93() V94() V95() Element of NAT
F is epsilon-transitive epsilon-connected ordinal natural V28() V29() ext-real non negative finite V41() countable V65() V67() V78() V79() V80() V81() V82() V83() V93() V94() V95() Element of NAT
F -tuples_on i is non empty functional with_common_domain product-like FinSequence-membered FinSequenceSet of i
{ b1 where b1 is Relation-like NAT -defined i -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of i * : len b1 = F } is set
g is set
F is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like set
len F is epsilon-transitive epsilon-connected ordinal natural V28() V29() ext-real non negative finite V41() countable V65() V67() V78() V79() V80() V81() V82() V83() V93() V94() V95() Element of NAT
F is Relation-like NAT -defined i -valued Function-like finite V43(F) countable FinSequence-like FinSubsequence-like Element of F -tuples_on i
i is non empty set
i * is non empty functional FinSequence-membered FinSequenceSet of i
K33((i *),i) is non empty Relation-like set
K32(K33((i *),i)) is non empty set
j is Relation-like i * -defined i -valued Function-like homogeneous Element of K32(K33((i *),i))
dom j is functional with_common_domain FinSequence-membered Element of K32((i *))
K32((i *)) is non empty set
arity j is epsilon-transitive epsilon-connected ordinal natural V28() V29() ext-real non negative finite V41() countable V65() V67() V78() V79() V80() V81() V82() V83() V93() V94() V95() Element of NAT
F is epsilon-transitive epsilon-connected ordinal natural V28() V29() ext-real non negative finite V41() countable V65() V67() V78() V79() V80() V81() V82() V83() V93() V94() V95() Element of NAT
F -tuples_on i is non empty functional with_common_domain product-like FinSequence-membered FinSequenceSet of i
{ b1 where b1 is Relation-like NAT -defined i -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of i * : len b1 = F } is set
g is set
ii is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like set
len ii is epsilon-transitive epsilon-connected ordinal natural V28() V29() ext-real non negative finite V41() countable V65() V67() V78() V79() V80() V81() V82() V83() V93() V94() V95() Element of NAT
F is Relation-like NAT -defined i -valued Function-like finite V43(F) countable FinSequence-like FinSubsequence-like Element of F -tuples_on i
i is Relation-like set
j is Relation-like Function-like set
rng i is set
F is Relation-like Function-like set
dom F is set
dom j is set
i is set
<*> i is empty Relation-like non-empty empty-yielding NAT -defined i -valued Function-like one-to-one constant functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V28() V29() ext-real non positive non negative finite finite-yielding V40() V41() V43( {} ) Cardinal-yielding with_common_domain countable FinSequence-like FinSubsequence-like FinSequence-membered complex-valued ext-real-valued real-valued natural-valued V78() V79() V80() V81() V82() V83() V84() Function-yielding V90() V93() V94() V95() V96() V97() homogeneous () FinSequence of i
i * is non empty functional FinSequence-membered FinSequenceSet of i
<*> i is empty Relation-like non-empty empty-yielding NAT -defined i -valued Function-like one-to-one constant functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V28() V29() ext-real non positive non negative finite finite-yielding V40() V41() V43( {} ) Cardinal-yielding with_common_domain countable FinSequence-like FinSubsequence-like FinSequence-membered complex-valued ext-real-valued real-valued natural-valued V78() V79() V80() V81() V82() V83() V84() Function-yielding V90() V93() V94() V95() V96() V97() homogeneous () FinSequence of i
j is Relation-like NAT -defined i -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of i *
i is Relation-like () set
rng i is set
j is Relation-like Function-like homogeneous set
arity j is epsilon-transitive epsilon-connected ordinal natural V28() V29() ext-real non negative finite V41() countable V65() V67() V78() V79() V80() V81() V82() V83() V93() V94() V95() Element of NAT
g is Relation-like Function-like homogeneous set
F is epsilon-transitive epsilon-connected ordinal natural V28() V29() ext-real non negative finite V41() countable V65() V67() V78() V79() V80() V81() V82() V83() V93() V94() V95() Element of NAT
arity g is epsilon-transitive epsilon-connected ordinal natural V28() V29() ext-real non negative finite V41() countable V65() V67() V78() V79() V80() V81() V82() V83() V93() V94() V95() Element of NAT
dom g is with_common_domain set
dom g is with_common_domain set
F is epsilon-transitive epsilon-connected ordinal natural V28() V29() ext-real non negative finite V41() countable V65() V67() V78() V79() V80() V81() V82() V83() V93() V94() V95() Element of NAT
arity g is epsilon-transitive epsilon-connected ordinal natural V28() V29() ext-real non negative finite V41() countable V65() V67() V78() V79() V80() V81() V82() V83() V93() V94() V95() Element of NAT
dom j is with_common_domain set
dom j is with_common_domain set
dom j is with_common_domain set
the Element of dom j is Element of dom j
dom g is with_common_domain set
ii is epsilon-transitive epsilon-connected ordinal natural V28() V29() ext-real non negative finite V41() countable V65() V67() V78() V79() V80() V81() V82() V83() V93() V94() V95() Element of NAT
k is non empty set
ii -tuples_on k is non empty functional with_common_domain product-like FinSequence-membered FinSequenceSet of k
k * is non empty functional FinSequence-membered FinSequenceSet of k
{ b1 where b1 is Relation-like NAT -defined k -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of k * : len b1 = ii } is set
k is Relation-like NAT -defined k -valued Function-like finite V43(ii) countable FinSequence-like FinSubsequence-like Element of ii -tuples_on k
len k is epsilon-transitive epsilon-connected ordinal natural V28() V29() ext-real non negative finite V41() countable V65() V67() V78() V79() V80() V81() V82() V83() V93() V94() V95() Element of NAT
the Element of dom g is Element of dom g
arity g is epsilon-transitive epsilon-connected ordinal natural V28() V29() ext-real non negative finite V41() countable V65() V67() V78() V79() V80() V81() V82() V83() V93() V94() V95() Element of NAT
k1 is Relation-like NAT -defined k -valued Function-like finite V43(ii) countable FinSequence-like FinSubsequence-like Element of ii -tuples_on k
len k1 is epsilon-transitive epsilon-connected ordinal natural V28() V29() ext-real non negative finite V41() countable V65() V67() V78() V79() V80() V81() V82() V83() V93() V94() V95() Element of NAT
F is epsilon-transitive epsilon-connected ordinal natural V28() V29() ext-real non negative finite V41() countable V65() V67() V78() V79() V80() V81() V82() V83() V93() V94() V95() Element of NAT
j is epsilon-transitive epsilon-connected ordinal natural V28() V29() ext-real non negative finite V41() countable V65() V67() V78() V79() V80() V81() V82() V83() V93() V94() V95() Element of NAT
F is epsilon-transitive epsilon-connected ordinal natural V28() V29() ext-real non negative finite V41() countable V65() V67() V78() V79() V80() V81() V82() V83() V93() V94() V95() Element of NAT
g is Relation-like Function-like homogeneous set
arity g is epsilon-transitive epsilon-connected ordinal natural V28() V29() ext-real non negative finite V41() countable V65() V67() V78() V79() V80() V81() V82() V83() V93() V94() V95() Element of NAT
i is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like () set
len i is epsilon-transitive epsilon-connected ordinal natural V28() V29() ext-real non negative finite V41() countable V65() V67() V78() V79() V80() V81() V82() V83() V93() V94() V95() Element of NAT
(i) is epsilon-transitive epsilon-connected ordinal natural V28() V29() ext-real non negative finite V41() countable V65() V67() V78() V79() V80() V81() V82() V83() V93() V94() V95() Element of NAT
rng i is finite countable set
j is Relation-like Function-like homogeneous set
i is set
i * is non empty functional FinSequence-membered FinSequenceSet of i
PFuncs ((i *),i) is non empty functional PartFunc-set of i * ,i
{ b1 where b1 is Relation-like i * -defined i -valued Function-like Element of PFuncs ((i *),i) : b1 is homogeneous } is set
K33((i *),i) is Relation-like set
K32(K33((i *),i)) is non empty set
F is set
g is Relation-like i * -defined i -valued Function-like Element of PFuncs ((i *),i)
F is non empty functional set
g is Relation-like Function-like Element of F
K33((i *),i) is Relation-like set
K32(K33((i *),i)) is non empty set
F is Relation-like i * -defined i -valued Function-like Element of PFuncs ((i *),i)
i is set
(i) is non empty functional PartFunc-set of i * ,i
i * is non empty functional FinSequence-membered FinSequenceSet of i
PFuncs ((i *),i) is non empty functional PartFunc-set of i * ,i
{ b1 where b1 is Relation-like i * -defined i -valued Function-like Element of PFuncs ((i *),i) : b1 is homogeneous } is set
K33((i *),i) is Relation-like set
K32(K33((i *),i)) is non empty set
F is Relation-like i * -defined i -valued Function-like Element of K32(K33((i *),i))
g is Relation-like i * -defined i -valued Function-like Element of PFuncs ((i *),i)
i is non empty set
i * is non empty functional FinSequence-membered FinSequenceSet of i
(i) is non empty functional PartFunc-set of i * ,i
PFuncs ((i *),i) is non empty functional PartFunc-set of i * ,i
{ b1 where b1 is Relation-like i * -defined i -valued Function-like Element of PFuncs ((i *),i) : b1 is homogeneous } is set
<*> i is empty proper Relation-like non-empty empty-yielding NAT -defined i -valued Function-like one-to-one constant functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V28() V29() ext-real non positive non negative finite finite-yielding V40() V41() V43( {} ) Cardinal-yielding with_common_domain countable FinSequence-like FinSubsequence-like FinSequence-membered complex-valued ext-real-valued real-valued natural-valued V78() V79() V80() V81() V82() V83() V84() Function-yielding V90() V93() V94() V95() V96() V97() homogeneous () FinSequence of i
K33(NAT,i) is non empty non trivial Relation-like non finite set
the Element of i is Element of i
K32((i *)) is non empty set
{(<*> i)} is non empty trivial functional finite V40() V43(1) with_common_domain countable V78() V79() V80() V81() V82() V83() V91() V92() V93() V94() V95() set
g is functional FinSequence-membered Element of K32((i *))
g --> the Element of i is Relation-like i * -defined g -defined i -valued Function-like constant total Element of PFuncs ((i *),i)
{ the Element of i} is non empty trivial finite V43(1) countable set
K33(g,{ the Element of i}) is Relation-like set
(<*> i) .--> the Element of i is non empty Relation-like {(<*> i)} -defined K32(K33(NAT,i)) -defined {(<*> i)} -defined i -valued Function-like one-to-one finite countable homogeneous set
K32(K33(NAT,i)) is non empty non trivial non finite set
{(<*> i)} --> the Element of i is non empty Relation-like {(<*> i)} -defined i -valued { the Element of i} -valued Function-like constant total quasi_total finite countable Element of K32(K33({(<*> i)},{ the Element of i}))
K33({(<*> i)},{ the Element of i}) is non empty Relation-like finite countable set
K32(K33({(<*> i)},{ the Element of i})) is non empty finite V40() countable set
{(<*> i)} --> the Element of i is non empty Relation-like {(<*> i)} -defined i -valued Function-like constant total quasi_total finite countable Element of K32(K33({(<*> i)},i))
K33({(<*> i)},i) is non empty Relation-like set
K32(K33({(<*> i)},i)) is non empty set
F is Relation-like i * -defined i -valued Function-like Element of (i)
dom F is functional FinSequence-membered Element of K32((i *))
ii is Relation-like NAT -defined i -valued Function-like finite countable FinSequence-like FinSubsequence-like FinSequence of i
len ii is epsilon-transitive epsilon-connected ordinal natural V28() V29() ext-real non negative finite V41() countable V65() V67() V78() V79() V80() V81() V82() V83() V93() V94() V95() Element of NAT
k is Relation-like NAT -defined i -valued Function-like finite countable FinSequence-like FinSubsequence-like FinSequence of i
len k is epsilon-transitive epsilon-connected ordinal natural V28() V29() ext-real non negative finite V41() countable V65() V67() V78() V79() V80() V81() V82() V83() V93() V94() V95() Element of NAT
dom F is functional FinSequence-membered set
i is set
i * is non empty functional FinSequence-membered FinSequenceSet of i
(i) is non empty functional PartFunc-set of i * ,i
PFuncs ((i *),i) is non empty functional PartFunc-set of i * ,i
{ b1 where b1 is Relation-like i * -defined i -valued Function-like Element of PFuncs ((i *),i) : b1 is homogeneous } is set
j is Relation-like i * -defined i -valued Function-like Element of (i)
F is Relation-like i * -defined i -valued Function-like Element of PFuncs ((i *),i)
i is non empty set
(i) is non empty functional PartFunc-set of i * ,i
i * is non empty functional FinSequence-membered FinSequenceSet of i
PFuncs ((i *),i) is non empty functional PartFunc-set of i * ,i
{ b1 where b1 is Relation-like i * -defined i -valued Function-like Element of PFuncs ((i *),i) : b1 is homogeneous } is set
K32((i)) is non empty set
j is non empty functional Element of K32((i))
F is Relation-like Function-like Element of j
(NAT) is non empty functional PartFunc-set of NAT * , NAT
PFuncs ((NAT *),NAT) is non empty functional PartFunc-set of NAT * , NAT
{ b1 where b1 is Relation-like NAT * -defined NAT -valued Function-like Element of PFuncs ((NAT *),NAT) : b1 is homogeneous } is set
i is Relation-like NAT * -defined RAT -valued Function-like complex-valued ext-real-valued real-valued natural-valued homogeneous set
rng i is V78() V79() V80() V81() V82() V83() V93() set
dom i is functional with_common_domain FinSequence-membered Element of K32((NAT *))
K32((NAT *)) is non empty set
j is Relation-like NAT * -defined NAT -valued Function-like complex-valued ext-real-valued real-valued natural-valued Element of PFuncs ((NAT *),NAT)
i is Relation-like NAT * -defined RAT -valued Function-like complex-valued ext-real-valued real-valued natural-valued homogeneous () set
j is Relation-like NAT * -defined NAT -valued Function-like complex-valued ext-real-valued real-valued natural-valued homogeneous Element of (NAT)
F is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued FinSequence of NAT
len F is epsilon-transitive epsilon-connected ordinal natural V28() V29() ext-real non negative finite V41() countable V65() V67() V78() V79() V80() V81() V82() V83() V93() V94() V95() Element of NAT
g is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued FinSequence of NAT
len g is epsilon-transitive epsilon-connected ordinal natural V28() V29() ext-real non negative finite V41() countable V65() V67() V78() V79() V80() V81() V82() V83() V93() V94() V95() Element of NAT
dom j is functional with_common_domain FinSequence-membered set
dom j is functional with_common_domain FinSequence-membered Element of K32((NAT *))
K32((NAT *)) is non empty set
i is non empty set
(i) is non empty functional PartFunc-set of i * ,i
i * is non empty functional FinSequence-membered FinSequenceSet of i
PFuncs ((i *),i) is non empty functional PartFunc-set of i * ,i
{ b1 where b1 is Relation-like i * -defined i -valued Function-like Element of PFuncs ((i *),i) : b1 is homogeneous } is set
j is Relation-like set
rng j is set
F is Relation-like Function-like set
g is Relation-like Function-like set
dom g is set
dom F is set
F is Relation-like i * -defined i -valued Function-like homogeneous Element of (i)
arity F is epsilon-transitive epsilon-connected ordinal natural V28() V29() ext-real non negative finite V41() countable V65() V67() V78() V79() V80() V81() V82() V83() V93() V94() V95() Element of NAT
ii is Relation-like i * -defined i -valued Function-like homogeneous Element of (i)
arity ii is epsilon-transitive epsilon-connected ordinal natural V28() V29() ext-real non negative finite V41() countable V65() V67() V78() V79() V80() V81() V82() V83() V93() V94() V95() Element of NAT
dom ii is functional with_common_domain FinSequence-membered Element of K32((i *))
K32((i *)) is non empty set
0