REAL is V66() V67() V68() V72() V79() V80() V82() set
NAT is V6() V7() V8() non empty non trivial non finite cardinal limit_cardinal countable denumerable V66() V67() V68() V69() V70() V71() V72() V77() V79() Element of bool REAL
bool REAL is non empty set
{} is Relation-like non-empty empty-yielding NAT -defined V6() V7() V8() V10() V11() V12() Function-like one-to-one constant functional empty ext-real V39() finite finite-yielding V44() cardinal {} -element Cardinal-yielding countable V53() V66() V67() V68() V69() V70() V71() V72() V79() V80() V81() V82() FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V89() constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding set
the Relation-like non-empty empty-yielding NAT -defined V6() V7() V8() V10() V11() V12() Function-like one-to-one constant functional empty ext-real V39() finite finite-yielding V44() cardinal {} -element Cardinal-yielding countable V53() V66() V67() V68() V69() V70() V71() V72() V79() V80() V81() V82() FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V89() constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding set is Relation-like non-empty empty-yielding NAT -defined V6() V7() V8() V10() V11() V12() Function-like one-to-one constant functional empty ext-real V39() finite finite-yielding V44() cardinal {} -element Cardinal-yielding countable V53() V66() V67() V68() V69() V70() V71() V72() V79() V80() V81() V82() FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V89() constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding set
1 is V6() V7() V8() V12() non empty ext-real positive V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V77() V78() V79() V80() V81() Element of NAT
[:1,1:] is Relation-like non empty finite countable set
bool [:1,1:] is non empty finite V44() countable set
[:[:1,1:],1:] is Relation-like non empty finite countable set
bool [:[:1,1:],1:] is non empty finite V44() countable set
NAT is V6() V7() V8() non empty non trivial non finite cardinal limit_cardinal countable denumerable V66() V67() V68() V69() V70() V71() V72() V77() V79() set
bool NAT is non empty non trivial non finite set
COMPLEX is V66() V72() set
RAT is V66() V67() V68() V69() V72() set
INT is V66() V67() V68() V69() V70() V72() set
bool NAT is non empty non trivial non finite set
[:COMPLEX,COMPLEX:] is Relation-like set
bool [:COMPLEX,COMPLEX:] is non empty set
[:COMPLEX,REAL:] is Relation-like set
bool [:COMPLEX,REAL:] is non empty set
{{},1} is non empty finite V44() countable V66() V67() V68() V69() V70() V71() V77() V78() V79() V80() V81() set
Trees is non empty constituted-Trees set
bool Trees is non empty set
FinTrees is non empty constituted-Trees constituted-FinTrees Element of bool Trees
[:[:COMPLEX,COMPLEX:],COMPLEX:] is Relation-like set
bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty set
[:REAL,REAL:] is Relation-like set
bool [:REAL,REAL:] is non empty set
[:[:REAL,REAL:],REAL:] is Relation-like set
bool [:[:REAL,REAL:],REAL:] is non empty set
[:RAT,RAT:] is Relation-like set
bool [:RAT,RAT:] is non empty set
[:[:RAT,RAT:],RAT:] is Relation-like set
bool [:[:RAT,RAT:],RAT:] is non empty set
[:INT,INT:] is Relation-like set
bool [:INT,INT:] is non empty set
[:[:INT,INT:],INT:] is Relation-like set
bool [:[:INT,INT:],INT:] is non empty set
[:NAT,NAT:] is Relation-like non empty non trivial non finite set
[:[:NAT,NAT:],NAT:] is Relation-like non empty non trivial non finite set
bool [:[:NAT,NAT:],NAT:] is non empty non trivial non finite set
K474() is set
2 is V6() V7() V8() V12() non empty ext-real positive V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V77() V78() V79() V80() V81() Element of NAT
3 is V6() V7() V8() V12() non empty ext-real positive V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V77() V78() V79() V80() V81() Element of NAT
Seg 1 is non empty trivial finite 1 -element countable V66() V67() V68() V69() V70() V71() V77() V78() V79() V80() V81() Element of bool NAT
curry {} is Relation-like Function-like set
curry' {} is Relation-like Function-like set
uncurry {} is Relation-like Function-like set
uncurry' {} is Relation-like Function-like set
{{}} is functional non empty trivial finite V44() 1 -element with_common_domain countable V66() V67() V68() V69() V70() V71() V77() V78() V79() V80() V81() Tree-like set
NAT * is functional non empty FinSequence-membered FinSequenceSet of NAT
<*> NAT is Relation-like non-empty empty-yielding NAT -defined NAT -valued V6() V7() V8() V10() V11() V12() Function-like one-to-one constant functional empty proper ext-real V39() finite finite-yielding V44() cardinal {} -element Cardinal-yielding countable V53() V66() V67() V68() V69() V70() V71() V72() V79() V80() V81() V82() FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V89() constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding FinSequence of NAT
0 is Relation-like non-empty empty-yielding NAT -defined V6() V7() V8() V10() V11() V12() Function-like one-to-one constant functional empty ext-real V39() finite finite-yielding V44() cardinal {} -element Cardinal-yielding countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V72() V79() V80() V81() V82() FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V89() constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding Element of NAT
product {} is functional non empty with_common_domain product-like set
F1() is non empty finite countable set
{ F2(b1) where b1 is Element of F1() : P1[b1] } is set
{ F2(b1) where b1 is Element of F1() : b1 in F1() } is set
X is set
X is Element of F1()
F2(X) is set
n is Relation-like Function-like set
proj1 n is set
proj2 n is set
X is set
{X} is non empty trivial finite 1 -element countable set
X is set
{X} is non empty trivial finite 1 -element countable set
[X,X] is V22() set
{X,X} is non empty finite countable set
{{X,X},{X}} is non empty finite V44() countable set
{[X,X]} is Relation-like Function-like constant non empty trivial finite 1 -element countable set
{X} --> X is Relation-like {X} -defined {X} -valued Function-like constant non empty total quasi_total finite countable Element of bool [:{X},{X}:]
[:{X},{X}:] is Relation-like non empty finite countable set
bool [:{X},{X}:] is non empty finite V44() countable set
n is set
<*> n is Relation-like non-empty empty-yielding NAT -defined n -valued V6() V7() V8() V10() V11() V12() Function-like one-to-one constant functional empty ext-real V39() finite finite-yielding V44() cardinal {} -element Cardinal-yielding countable V53() V66() V67() V68() V69() V70() V71() V72() V79() V80() V81() V82() FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V89() constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding FinSequence of n
X is Relation-like n -defined Function-like total set
X # is Relation-like n * -defined Function-like non empty total set
n * is functional non empty FinSequence-membered FinSequenceSet of n
(X #) . (<*> n) is set
X is Relation-like NAT -defined n -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of n *
X * X is Relation-like NAT -defined Function-like finite countable set
product (X * X) is functional with_common_domain product-like set
F1() is set
n is set
F2(n) is set
F3(n) is set
n is Relation-like F1() -defined Function-like total set
X is Element of F1()
n . X is set
F2(X) is set
F3(X) is set
n is set
n --> {{}} is Relation-like non-empty n -defined {{{}}} -valued Function-like constant total quasi_total Element of bool [:n,{{{}}}:]
{{{}}} is non empty trivial finite V44() 1 -element countable set
[:n,{{{}}}:] is Relation-like set
bool [:n,{{{}}}:] is non empty set
X is Relation-like Function-like set
X is Relation-like n -defined Function-like total set
m is set
X . m is set
n is set
bool n is non empty set
X is Element of bool n
X is Relation-like n -defined Function-like total set
X | X is Relation-like X -defined n -defined Function-like set
proj1 (X | X) is set
proj1 X is set
(proj1 X) /\ X is Element of bool n
k is Relation-like X -defined Function-like set
n is set
bool n is non empty set
X is Element of bool n
X is Relation-like n -defined Function-like total set
X | X is Relation-like X -defined n -defined Function-like total set
n is Relation-like non-empty Function-like set
X is set
n | X is Relation-like Function-like set
proj2 (n | X) is set
proj2 n is set
n is non empty set
X is Relation-like non-empty non empty-yielding n -defined Function-like non empty total set
proj2 X is non empty set
union (proj2 X) is set
the Element of n is Element of n
proj1 X is non empty set
X . the Element of n is non empty set
n is set
n --> {} is Relation-like n -defined {{}} -valued Function-like constant total quasi_total Cardinal-yielding Function-yielding V89() Element of bool [:n,{{}}:]
[:n,{{}}:] is Relation-like set
bool [:n,{{}}:] is non empty set
uncurry (n --> {}) is Relation-like Function-like set
proj2 (n --> {}) is trivial finite countable set
Funcs ({},{}) is set
proj1 (uncurry (n --> {})) is set
proj1 (n --> {}) is set
[:(proj1 (n --> {})),{}:] is Relation-like set
n is non empty set
X is set
n --> X is Relation-like n -defined {X} -valued Function-like constant non empty total quasi_total Element of bool [:n,{X}:]
{X} is non empty trivial finite 1 -element countable set
[:n,{X}:] is Relation-like non empty set
bool [:n,{X}:] is non empty set
X is Relation-like non-empty non empty-yielding n -defined Function-like non empty total set
m is Relation-like n -defined Function-like non empty total Function-yielding V89() ManySortedFunction of n --> X,X
commute m is Relation-like Function-like Function-yielding V89() set
proj1 (commute m) is set
proj1 X is non empty set
proj1 m is non empty set
proj2 m is non empty set
k is set
C is set
m . C is Relation-like Function-like set
(n --> X) . C is set
X . C is set
[:((n --> X) . C),(X . C):] is Relation-like set
bool [:((n --> X) . C),(X . C):] is non empty set
n --> {} is Relation-like n -defined {{}} -valued Function-like constant non empty total quasi_total Cardinal-yielding Function-yielding V89() Element of bool [:n,{{}}:]
[:n,{{}}:] is Relation-like non empty set
bool [:n,{{}}:] is non empty set
uncurry m is Relation-like Function-like set
curry' (uncurry m) is Relation-like Function-like set
proj2 m is non empty set
proj2 X is non empty set
union (proj2 X) is set
Funcs (X,(union (proj2 X))) is set
k is set
C is set
m . C is Relation-like Function-like set
(n --> X) . C is set
X . C is set
[:X,(X . C):] is Relation-like set
bool [:X,(X . C):] is non empty set
A is Relation-like X -defined X . C -valued Function-like quasi_total Element of bool [:X,(X . C):]
proj2 A is set
proj1 A is set
Funcs (n,(Funcs (X,(union (proj2 X))))) is set
Funcs (n,(union (proj2 X))) is set
Funcs (X,(Funcs (n,(union (proj2 X))))) is set
[:X,(Funcs (n,(union (proj2 X)))):] is Relation-like set
bool [:X,(Funcs (n,(union (proj2 X)))):] is non empty set
F1() is non empty set
[:NAT,F1():] is Relation-like non empty non trivial non finite set
bool [:NAT,F1():] is non empty non trivial non finite set
F2() is Element of F1()
n is Relation-like NAT -defined F1() -valued Function-like quasi_total Element of bool [:NAT,F1():]
n . {} is Element of F1()
X is Relation-like NAT -defined F1() -valued Function-like quasi_total Element of bool [:NAT,F1():]
X . {} is Element of F1()
F1() is non empty set
bool F1() is non empty set
F2() is Element of bool F1()
F3() is Relation-like F2() -defined Function-like total set
F4() is Relation-like F2() -defined Function-like total set
n is Relation-like F2() -defined Function-like total set
X is set
proj1 n is set
n . X is set
F5(X) is set
X is Relation-like F2() -defined Function-like total Function-yielding V89() set
X is set
X . X is Relation-like Function-like set
F3() . X is set
F4() . X is set
[:(F3() . X),(F4() . X):] is Relation-like set
bool [:(F3() . X),(F4() . X):] is non empty set
F5(X) is set
X is Relation-like F2() -defined Function-like total Function-yielding V89() ManySortedFunction of F3(),F4()
m is Element of F1()
X . m is Relation-like Function-like set
F5(m) is set
n is set
X is Relation-like non-empty n -defined Function-like total set
product X is functional non empty with_common_domain product-like set
proj1 X is set
X is Relation-like Function-like set
proj1 X is set
m is Relation-like n -defined Function-like X -compatible total Element of product X
m +* X is Relation-like Function-like set
k is set
(m +* X) . k is set
X . k is set
X . k is set
(m +* X) . k is set
m . k is set
X . k is set
C is Relation-like Function-like set
proj1 C is set
proj1 (m +* X) is set
proj1 m is set
(proj1 m) \/ (proj1 X) is set
n is non empty set
X is non empty set
n --> X is Relation-like non-empty non empty-yielding n -defined {X} -valued Function-like constant non empty total quasi_total Element of bool [:n,{X}:]
{X} is non empty trivial finite 1 -element countable set
[:n,{X}:] is Relation-like non empty set
bool [:n,{X}:] is non empty set
X is Relation-like non-empty non empty-yielding n -defined Function-like non empty total set
m is Relation-like n -defined Function-like non empty total Function-yielding V89() ManySortedFunction of n --> X,X
commute m is Relation-like Function-like Function-yielding V89() set
k is Element of X
(commute m) . k is Relation-like Function-like set
proj1 m is non empty set
uncurry m is Relation-like Function-like set
proj1 (uncurry m) is set
[:n,X:] is Relation-like non empty set
C is set
A is set
C is set
[A,C] is V22() set
{A,C} is non empty finite countable set
{A} is non empty trivial finite 1 -element countable set
{{A,C},{A}} is non empty finite V44() countable set
B is Relation-like Function-like set
m . A is Relation-like Function-like set
proj1 B is set
(n --> X) . A is set
X . A is set
[:((n --> X) . A),(X . A):] is Relation-like set
bool [:((n --> X) . A),(X . A):] is non empty set
C is set
A is set
[C,A] is V22() set
{C,A} is non empty finite countable set
{C} is non empty trivial finite 1 -element countable set
{{C,A},{C}} is non empty finite V44() countable set
[C,A] `1 is set
m . ([C,A] `1) is Relation-like Function-like set
B is Relation-like Function-like set
(n --> X) . ([C,A] `1) is set
X . ([C,A] `1) is set
[:((n --> X) . ([C,A] `1)),(X . ([C,A] `1)):] is Relation-like set
bool [:((n --> X) . ([C,A] `1)),(X . ([C,A] `1)):] is non empty set
proj1 B is set
[C,A] `2 is set
curry' (uncurry m) is Relation-like Function-like set
(curry' (uncurry m)) . k is set
proj2 (uncurry m) is set
A is Relation-like Function-like set
proj1 A is set
proj2 A is set
C is Relation-like n -defined Function-like non empty total set
A is set
C . A is set
X . A is set
m . A is Relation-like Function-like set
(n --> X) . A is set
B is Relation-like Function-like set
[:X,(X . A):] is Relation-like set
bool [:X,(X . A):] is non empty set
proj1 B is set
(uncurry m) . (A,k) is set
B . k is set
C is Relation-like Function-like set
proj1 C is set
proj2 C is set
n is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT
X is set
{X} is non empty trivial finite 1 -element countable set
n |-> {X} is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like set
Seg n is finite n -element countable V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of bool NAT
(Seg n) --> {X} is Relation-like non-empty Seg n -defined {{X}} -valued Function-like constant total quasi_total finite countable Element of bool [:(Seg n),{{X}}:]
{{X}} is non empty trivial finite V44() 1 -element countable set
[:(Seg n),{{X}}:] is Relation-like finite countable set
bool [:(Seg n),{{X}}:] is non empty finite V44() countable set
product (n |-> {X}) is functional with_common_domain product-like set
n |-> X is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like set
(Seg n) --> X is Relation-like Seg n -defined {X} -valued Function-like constant total quasi_total finite countable Element of bool [:(Seg n),{X}:]
[:(Seg n),{X}:] is Relation-like finite countable set
bool [:(Seg n),{X}:] is non empty finite V44() countable set
{(n |-> X)} is functional non empty trivial finite V44() 1 -element with_common_domain countable set
X is set
dom (n |-> {X}) is finite countable V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of bool NAT
m is Relation-like Function-like set
proj1 m is set
k is set
m . k is set
(n |-> {X}) . k is set
k is set
m is Relation-like Function-like set
m . k is set
(n |-> {X}) . k is set
proj1 m is set
n is non empty set
FinTrees n is functional non empty constituted-DTrees DTree-set of n
X is Relation-like n -valued Function-like DecoratedTree-like Element of FinTrees n
proj1 X is non empty finite countable Tree-like set
n is Relation-like Function-like finite countable DecoratedTree-like set
proj1 n is non empty finite countable Tree-like set
X is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of proj1 n
n | X is Relation-like Function-like DecoratedTree-like set
proj1 (n | X) is non empty Tree-like set
(proj1 n) | X is non empty finite countable Tree-like set
n is non empty finite countable Tree-like set
X is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of n
n | X is non empty finite countable Tree-like set
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of n : X c= b1 } is set
m is Relation-like Function-like set
proj1 m is set
proj2 m is set
k is set
m . k is set
C is set
m . C is set
A is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of n | X
X ^ A is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like FinSequence of NAT
B is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of n | X
m . B is set
X ^ B is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like FinSequence of NAT
k is set
C is set
m . C is set
A is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of n | X
X ^ A is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like FinSequence of NAT
m . A is set
B is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of n
k is set
C is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of n
C is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like set
X ^ C is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like set
A is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of n
B is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of n
A is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of n | X
m . A is set
n is Relation-like Function-like finite countable DecoratedTree-like set
proj1 n is non empty finite countable Tree-like set
X is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of proj1 n
X is Relation-like Function-like finite countable DecoratedTree-like set
n with-replacement (X,X) is Relation-like Function-like DecoratedTree-like set
proj1 (n with-replacement (X,X)) is non empty Tree-like set
proj1 X is non empty finite countable Tree-like set
(proj1 n) with-replacement (X,(proj1 X)) is non empty finite countable Tree-like set
n is non empty finite countable Tree-like set
X is non empty finite countable Tree-like set
X is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of n
n with-replacement (X,X) is non empty finite countable Tree-like set
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of n : not X c= b1 } is set
{ (X ^ b1) where b1 is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of X : verum } is set
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of n : not X c= b1 } \/ { (X ^ b1) where b1 is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of X : verum } is set
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of n : not X c< b1 } is set
{ H1(b1) where b1 is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of X : S2[b1] } is set
{ H1(b1) where b1 is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of X : S1[b1] } is set
B is set
C is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of n
{X} is functional non empty trivial finite V44() 1 -element with_common_domain countable set
C is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of n
C is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of n
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of n : not X c= b1 } \/ {X} is non empty set
X ^ {} is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like set
B is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of X
C is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of X
( { b1 where b1 is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of n : not X c= b1 } \/ {X}) \/ { H1(b1) where b1 is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of X : S1[b1] } is non empty set
{X} \/ { H1(b1) where b1 is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of X : S1[b1] } is non empty set
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of n : not X c= b1 } \/ ({X} \/ { H1(b1) where b1 is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of X : S1[b1] } ) is non empty set
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of n : not X c= b1 } \/ { H1(b1) where b1 is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of X : S1[b1] } is set
n is non empty finite countable Tree-like set
X is non empty finite countable Tree-like set
X is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of n
n with-replacement (X,X) is non empty finite countable Tree-like set
m is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like FinSequence of NAT
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of n : not X c= b1 } is set
k is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of n
{ (X ^ b1) where b1 is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of X : verum } is set
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of n : not X c= b1 } \/ { (X ^ b1) where b1 is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of X : verum } is set
n is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like Tree-yielding set
dom n is finite countable V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of bool NAT
tree n is non empty Tree-like set
X is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT
X + 1 is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT
<*X*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element countable FinSequence-like FinSubsequence-like FinSequence of NAT
(tree n) | <*X*> is non empty Tree-like set
n . (X + 1) is set
len n is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT
n is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like DTree-yielding set
dom n is finite countable V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of bool NAT
doms n is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like Tree-yielding set
tree (doms n) is non empty Tree-like set
X is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT
X + 1 is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT
<*X*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element countable FinSequence-like FinSubsequence-like FinSequence of NAT
len n is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT
Seg (len n) is finite len n -element countable V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of bool NAT
len (doms n) is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT
Seg (len (doms n)) is finite len (doms n) -element countable V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of bool NAT
dom (doms n) is finite countable V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of bool NAT
(doms n) . (X + 1) is set
<*X*> ^ {} is Relation-like NAT -defined Function-like non empty finite countable FinSequence-like FinSubsequence-like set
n is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like Tree-yielding set
len n is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT
X is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like Tree-yielding set
len X is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT
dom n is finite countable V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of bool NAT
tree X is non empty Tree-like set
tree n is non empty Tree-like set
X is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT
X + 1 is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT
X . (X + 1) is set
<*X*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element countable FinSequence-like FinSubsequence-like FinSequence of NAT
m is non empty Tree-like set
(tree n) with-replacement (<*X*>,m) is non empty Tree-like set
C is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like FinSequence of NAT
A is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT
B is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like set
A + 1 is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT
X . (A + 1) is set
<*A*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element countable FinSequence-like FinSubsequence-like FinSequence of NAT
<*A*> ^ B is Relation-like NAT -defined Function-like non empty finite countable FinSequence-like FinSubsequence-like set
A is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT
B is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like set
A + 1 is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT
X . (A + 1) is set
<*A*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element countable FinSequence-like FinSubsequence-like FinSequence of NAT
<*A*> ^ B is Relation-like NAT -defined Function-like non empty finite countable FinSequence-like FinSubsequence-like set
C is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like FinSequence of NAT
t is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like FinSequence of NAT
<*X*> ^ t is Relation-like NAT -defined NAT -valued Function-like non empty finite countable FinSequence-like FinSubsequence-like FinSequence of NAT
n . (A + 1) is set
C . 1 is set
C is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like set
<*X*> ^ C is Relation-like NAT -defined Function-like non empty finite countable FinSequence-like FinSubsequence-like set
C is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like FinSequence of NAT
<*X*> ^ C is Relation-like NAT -defined NAT -valued Function-like non empty finite countable FinSequence-like FinSubsequence-like FinSequence of NAT
A is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT
B is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like set
A + 1 is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT
n . (A + 1) is set
<*A*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element countable FinSequence-like FinSubsequence-like FinSequence of NAT
<*A*> ^ B is Relation-like NAT -defined Function-like non empty finite countable FinSequence-like FinSubsequence-like set
A is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT
B is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like set
A + 1 is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT
n . (A + 1) is set
<*A*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element countable FinSequence-like FinSubsequence-like FinSequence of NAT
<*A*> ^ B is Relation-like NAT -defined Function-like non empty finite countable FinSequence-like FinSubsequence-like set
dom X is finite countable V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of bool NAT
X . (A + 1) is set
X . (A + 1) is set
A is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like FinSequence of NAT
<*X*> ^ A is Relation-like NAT -defined NAT -valued Function-like non empty finite countable FinSequence-like FinSubsequence-like FinSequence of NAT
A is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like FinSequence of NAT
<*X*> ^ A is Relation-like NAT -defined NAT -valued Function-like non empty finite countable FinSequence-like FinSubsequence-like FinSequence of NAT
n . (X + 1) is set
<*X*> ^ {} is Relation-like NAT -defined Function-like non empty finite countable FinSequence-like FinSubsequence-like set
n is Relation-like Function-like finite countable DecoratedTree-like set
proj1 n is non empty finite countable Tree-like set
X is Relation-like Function-like finite countable DecoratedTree-like set
X is set
m is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT
<*m*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element countable FinSequence-like FinSubsequence-like FinSequence of NAT
n with-replacement (<*m*>,X) is Relation-like Function-like DecoratedTree-like set
m + 1 is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT
k is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like DTree-yielding set
X -tree k is Relation-like Function-like DecoratedTree-like set
len k is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT
dom k is finite countable V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of bool NAT
A is Relation-like Function-like DecoratedTree-like set
proj1 A is non empty Tree-like set
C is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT
C + 1 is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT
k . (C + 1) is set
<*C*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element countable FinSequence-like FinSubsequence-like FinSequence of NAT
B is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of proj1 A
<*C*> ^ B is Relation-like NAT -defined NAT -valued Function-like non empty finite countable FinSequence-like FinSubsequence-like FinSequence of NAT
proj1 (X -tree k) is non empty Tree-like set
C is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like DTree-yielding set
doms C is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like Tree-yielding set
tree (doms C) is non empty Tree-like set
dom (doms C) is finite countable V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of bool NAT
n is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like set
len n is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT
dom n is finite countable V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of bool NAT
Seg (len k) is finite len k -element countable V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of bool NAT
q is set
qq is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT
n . qq is set
k . qq is set
IFEQ (qq,(m + 1),X,(k . qq)) is set
n . q is set
q is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like DTree-yielding set
X -tree q is Relation-like Function-like DecoratedTree-like set
proj1 (X -tree q) is non empty Tree-like set
qq is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like DTree-yielding set
doms qq is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like Tree-yielding set
tree (doms qq) is non empty Tree-like set
len (doms C) is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT
len (doms qq) is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT
dqq is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT
q . dqq is set
k . dqq is set
IFEQ (dqq,(m + 1),X,(k . dqq)) is set
(doms C) . dqq is set
i is Relation-like Function-like DecoratedTree-like set
proj1 i is non empty Tree-like set
(doms qq) . dqq is set
len q is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT
q . (m + 1) is set
<*m*> . 1 is set
k . (m + 1) is set
IFEQ ((m + 1),(m + 1),X,(k . (m + 1))) is set
(doms qq) . (m + 1) is set
proj1 X is non empty finite countable Tree-like set
(proj1 n) with-replacement (<*m*>,(proj1 X)) is non empty Tree-like set
f is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like FinSequence of NAT
(X -tree q) . f is set
n . f is set
i is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of proj1 n
dqq is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like Tree-yielding set
len dqq is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT
doms q is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like Tree-yielding set
len (doms q) is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT
r is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT
r is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like set
r + 1 is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT
dqq . (r + 1) is set
<*r*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element countable FinSequence-like FinSubsequence-like FinSequence of NAT
<*r*> ^ r is Relation-like NAT -defined Function-like non empty finite countable FinSequence-like FinSubsequence-like set
r is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT
r is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like set
r + 1 is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT
(doms q) . (r + 1) is set
<*r*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element countable FinSequence-like FinSubsequence-like FinSequence of NAT
<*r*> ^ r is Relation-like NAT -defined Function-like non empty finite countable FinSequence-like FinSubsequence-like set
(X -tree q) | <*r*> is Relation-like Function-like DecoratedTree-like set
q . (r + 1) is set
k . (r + 1) is set
IFEQ ((r + 1),(m + 1),X,(k . (r + 1))) is set
doms k is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like Tree-yielding set
dom (doms k) is finite countable V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of bool NAT
(proj1 (X -tree k)) | <*r*> is non empty Tree-like set
(doms k) . (r + 1) is set
pw1 is Relation-like Function-like DecoratedTree-like set
proj1 pw1 is non empty Tree-like set
c22 is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like DTree-yielding set
doms c22 is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like Tree-yielding set
tree (doms c22) is non empty Tree-like set
dom (doms q) is finite countable V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of bool NAT
(proj1 (X -tree q)) | <*r*> is non empty Tree-like set
ww is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like FinSequence of NAT
(X -tree q) | ww is Relation-like Function-like DecoratedTree-like set
c19 is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like FinSequence of NAT
((X -tree q) | ww) . c19 is set
(X -tree k) | ww is Relation-like Function-like DecoratedTree-like set
((X -tree k) | ww) . c19 is set
dqq is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like Tree-yielding set
len dqq is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT
i is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of proj1 n
r is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of proj1 X
i ^ r is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like FinSequence of NAT
r is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of proj1 X
<*m*> ^ r is Relation-like NAT -defined NAT -valued Function-like non empty finite countable FinSequence-like FinSubsequence-like FinSequence of NAT
(X -tree q) | <*m*> is Relation-like Function-like DecoratedTree-like set
r is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like FinSequence of NAT
<*m*> ^ r is Relation-like NAT -defined NAT -valued Function-like non empty finite countable FinSequence-like FinSubsequence-like FinSequence of NAT
X . r is set
(proj1 (X -tree q)) | <*m*> is non empty Tree-like set
i is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of proj1 n
i is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT
q . i is set
k . i is set
IFEQ (i,(m + 1),X,(k . i)) is set
n is non empty finite countable Tree-like set
card n is V6() V7() V8() V12() non empty ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V77() V78() V79() V80() V81() Element of NAT
X is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of n
n | X is non empty finite countable Tree-like set
card (n | X) is V6() V7() V8() V12() non empty ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V77() V78() V79() V80() V81() Element of NAT
X is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of NAT *
{ (X ^ b1) where b1 is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of NAT * : b1 in n | X } is set
k is Relation-like Function-like set
proj1 k is set
proj2 k is set
C is set
k . C is set
A is set
k . A is set
B is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of n | X
X ^ B is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like FinSequence of NAT
C is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of n | X
k . C is set
X ^ C is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like FinSequence of NAT
C is set
A is set
k . A is set
B is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of NAT *
k . B is set
X ^ B is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like FinSequence of NAT
C is set
A is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of NAT *
X ^ A is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like FinSequence of NAT
B is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of n | X
k . B is set
k is finite countable set
card k is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT
C is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of NAT *
X ^ C is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like FinSequence of NAT
C is set
A is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of NAT *
X ^ A is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like FinSequence of NAT
n is non empty finite countable Tree-like set
card n is V6() V7() V8() V12() non empty ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V77() V78() V79() V80() V81() Element of NAT
X is non empty finite countable Tree-like set
card X is V6() V7() V8() V12() non empty ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V77() V78() V79() V80() V81() Element of NAT
(card n) + (card X) is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT
X is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of n
n with-replacement (X,X) is non empty finite countable Tree-like set
card (n with-replacement (X,X)) is V6() V7() V8() V12() non empty ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V77() V78() V79() V80() V81() Element of NAT
n | X is non empty finite countable Tree-like set
card (n | X) is V6() V7() V8() V12() non empty ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V77() V78() V79() V80() V81() Element of NAT
(card (n with-replacement (X,X))) + (card (n | X)) is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of n : S1[b1] } is set
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of n : S2[b1] } is set
{ (X ^ b1) where b1 is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of X : verum } is set
bool n is non empty finite V44() countable set
A is Relation-like Function-like set
proj1 A is set
proj2 A is set
B is set
A . B is set
C is set
A . C is set
t is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of X
X ^ t is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like FinSequence of NAT
n is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of X
A . n is set
X ^ n is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like FinSequence of NAT
B is set
C is set
A . C is set
t is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of NAT *
A . t is set
X ^ t is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like FinSequence of NAT
B is set
C is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of X
X ^ C is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like FinSequence of NAT
A . C is set
C is set
t is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of n
A is finite countable set
B is finite countable set
A \/ B is finite countable set
A /\ { (X ^ b1) where b1 is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of X : verum } is finite countable set
C is set
t is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of n
n is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of X
X ^ n is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like FinSequence of NAT
A /\ B is finite countable set
C is set
t is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of n
n is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of n
A \/ { (X ^ b1) where b1 is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of X : verum } is set
C is finite countable set
card C is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT
card B is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT
card A is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT
(card A) + (card C) is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT
((card A) + (card C)) + (card B) is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT
(card A) + (card B) is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT
((card A) + (card B)) + (card C) is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT
n is Relation-like Function-like finite countable DecoratedTree-like set
proj1 n is non empty finite countable Tree-like set
X is Relation-like Function-like finite countable DecoratedTree-like set
card n is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT
card X is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT
(card n) + (card X) is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT
X is Relation-like NAT -defined NAT -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of proj1 n
n with-replacement (X,X) is Relation-like Function-like finite countable DecoratedTree-like set
card (n with-replacement (X,X)) is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT
n | X is Relation-like Function-like finite countable DecoratedTree-like set
card (n | X) is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT
(card (n with-replacement (X,X))) + (card (n | X)) is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT
card (proj1 n) is V6() V7() V8() V12() non empty ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V77() V78() V79() V80() V81() Element of NAT
proj1 X is non empty finite countable Tree-like set
card (proj1 X) is V6() V7() V8() V12() non empty ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V77() V78() V79() V80() V81() Element of NAT
proj1 (n with-replacement (X,X)) is non empty finite countable Tree-like set
card (proj1 (n with-replacement (X,X))) is V6() V7() V8() V12() non empty ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V77() V78() V79() V80() V81() Element of NAT
proj1 (n | X) is non empty finite countable Tree-like set
card (proj1 (n | X)) is V6() V7() V8() V12() non empty ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V77() V78() V79() V80() V81() Element of NAT
(proj1 n) with-replacement (X,(proj1 X)) is non empty finite countable Tree-like set
(proj1 n) | X is non empty finite countable Tree-like set
n is set
root-tree n is Relation-like Function-like DecoratedTree-like set
[{},n] is V22() set
{{},n} is non empty finite countable set
{{{},n},{{}}} is non empty finite V44() countable set
{[{},n]} is Relation-like Function-like constant non empty trivial finite 1 -element countable set
n is set
root-tree n is Relation-like Function-like finite countable DecoratedTree-like set
card (root-tree n) is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT
[{},n] is V22() set
{{},n} is non empty finite countable set
{{{},n},{{}}} is non empty finite V44() countable set
{[{},n]} is Relation-like Function-like constant non empty trivial finite 1 -element countable set
n is non empty finite countable set
card n is V6() V7() V8() V12() non empty ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V77() V78() V79() V80() V81() Element of NAT
(card n) - 1 is ext-real V39() V53() set
(card n) -' 1 is ext-real non negative V39() V53() set
n is Relation-like Function-like set
proj1 n is set
X is Relation-like Function-like set
proj1 X is set
card n is V6() V7() V8() cardinal set
card (proj1 n) is V6() V7() V8() cardinal set
card X is V6() V7() V8() cardinal set
card (proj1 X) is V6() V7() V8() cardinal set
n is Relation-like Function-like finite countable set
proj1 n is finite countable set
X is Relation-like Function-like finite countable set
proj1 X is finite countable set
n +* X is Relation-like Function-like finite countable set
card (n +* X) is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT
card n is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT
card X is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT
(card n) + (card X) is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT
proj1 (n +* X) is finite countable set
card (proj1 (n +* X)) is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT
(proj1 n) \/ (proj1 X) is finite countable set
card ((proj1 n) \/ (proj1 X)) is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT
card (proj1 n) is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT
card (proj1 X) is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT
(card (proj1 n)) + (card (proj1 X)) is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT
(card (proj1 n)) + (card X) is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT
n is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() set
{ b1 where b1 is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT : not b1 <= n } is set
X is set
m is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT
n + 1 is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT
n + {} is ext-real V39() V53() set
X is non empty finite countable V66() V67() V68() V69() V70() V71() V77() V78() V79() V80() V81() Element of bool NAT
max X is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() set
k is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT
k + 1 is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT
k + {} is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT
(max X) + 1 is V6() V7() V8() V12() ext-real V39() finite cardinal countable V53() V64() V65() V66() V67() V68() V69() V70() V71() V79() V80() V81() Element of NAT
(max X) + {} is ext-real V39() V53() set