REAL is non empty non trivial non finite set
NAT is epsilon-transitive epsilon-connected ordinal non empty non trivial non finite cardinal limit_cardinal Element of bool REAL
bool REAL is non empty non trivial non finite set
omega is epsilon-transitive epsilon-connected ordinal non empty non trivial non finite cardinal limit_cardinal set
bool omega is non empty non trivial non finite set
bool NAT is non empty non trivial non finite set
{} is Relation-like non-empty empty-yielding NAT -defined epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like one-to-one constant functional empty Function-yielding V32() ext-real non positive non negative V36() V37() finite finite-yielding V42() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered set
the Relation-like non-empty empty-yielding NAT -defined epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like one-to-one constant functional empty Function-yielding V32() ext-real non positive non negative V36() V37() finite finite-yielding V42() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered set is Relation-like non-empty empty-yielding NAT -defined epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like one-to-one constant functional empty Function-yielding V32() ext-real non positive non negative V36() V37() finite finite-yielding V42() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered set
1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V36() V37() finite cardinal Element of NAT
2 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V36() V37() finite cardinal Element of NAT
3 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V36() V37() finite cardinal Element of NAT
0 is Relation-like non-empty empty-yielding NAT -defined epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like one-to-one constant functional empty Function-yielding V32() ext-real non positive non negative V36() V37() finite finite-yielding V42() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered Element of NAT
Seg 1 is non empty trivial finite 1 -element Element of bool NAT
NAT * is functional non empty FinSequence-membered FinSequenceSet of NAT
<*> NAT is Relation-like non-empty empty-yielding NAT -defined NAT -valued epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like one-to-one constant functional empty proper Function-yielding V32() ext-real non positive non negative V36() V37() finite finite-yielding V42() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of NAT
[:NAT,NAT:] is Relation-like non empty non trivial non finite set
union {} is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal set
card {} is Relation-like non-empty empty-yielding NAT -defined epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like one-to-one constant functional empty Function-yielding V32() ext-real non positive non negative V36() V37() finite finite-yielding V42() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered set
X is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
B is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
Y is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len X is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
len Y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
f is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
X ^ f is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
D is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
Y ^ D is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
f is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
X ^ f is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
D is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
Y ^ D is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
X is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
B is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
Y is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
X is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
X + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V36() V37() finite cardinal Element of NAT
Y is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len Y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
Seg X is finite X -element Element of bool NAT
Y | (Seg X) is Relation-like NAT -defined Seg X -defined NAT -defined Function-like finite FinSubsequence-like set
B is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
f is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
B ^ f is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len B is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
f . 1 is set
<*(f . 1)*> is Relation-like NAT -defined Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like set
B ^ <*(f . 1)*> is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set
len f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
X + (len f) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
X is set
<*X*> is Relation-like NAT -defined Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like set
Y is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
Y ^ <*X*> is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set
ProperPrefixes (Y ^ <*X*>) is finite set
ProperPrefixes Y is finite set
{Y} is functional non empty trivial finite V42() 1 -element set
(ProperPrefixes Y) \/ {Y} is non empty finite set
B is set
f is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
B is set
f is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
Y ^ {} is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
F1() is non empty Tree-like set
X is set
card X is epsilon-transitive epsilon-connected ordinal cardinal set
X is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of F1()
len X is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
X is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
X + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V36() V37() finite cardinal Element of NAT
Y is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of F1()
len Y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
B is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
f is set
<*f*> is Relation-like NAT -defined Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like set
B ^ <*f*> is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set
len B is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
D is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
rng <*f*> is non empty trivial finite 1 -element set
rng Y is finite Element of bool NAT
{f} is non empty trivial finite 1 -element set
x is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of F1()
g is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
X is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of F1()
len X is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
X is non empty Tree-like set
Y is non empty Tree-like set
B is set
f is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X
B is set
f is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of Y
X is non empty Tree-like set
Y is non empty Tree-like set
B is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
f is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
X is non empty Tree-like set
Y is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
X | Y is non empty Tree-like set
X with-replacement (Y,(X | Y)) is non empty Tree-like set
B is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
f is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
Y ^ f is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
rng f is finite set
rng B is finite Element of bool NAT
D is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
x is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
Y ^ x is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
f is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
Y ^ f is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
f is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
Y ^ f is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
X is non empty Tree-like set
Y is non empty Tree-like set
B is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
X with-replacement (B,Y) is non empty Tree-like set
f is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
X is non empty Tree-like set
Y is non empty Tree-like set
B is non empty Tree-like set
f is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
X with-replacement (f,Y) is non empty Tree-like set
D is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
(X with-replacement (f,Y)) with-replacement (D,B) is non empty Tree-like set
X with-replacement (D,B) is non empty Tree-like set
(X with-replacement (D,B)) with-replacement (f,Y) is non empty Tree-like set
x is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
g is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
D ^ g is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
g is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
f ^ g is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
y is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
D ^ y is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
g is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
f ^ g is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
g is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
f ^ g is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
g is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
D ^ g is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
y is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
f ^ y is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
g is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
D ^ g is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
{{}} is functional non empty trivial finite V42() 1 -element Tree-like set
X is non empty Tree-like set
<*0*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
Y is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X
Y ^ <*0*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
X is non empty Tree-like set
bool X is non empty set
Y is Element of bool X
B is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
f is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
{{}} is functional non empty trivial finite V42() 1 -element Tree-like set
Y is Element of bool X
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X : len b1 = 0 } is set
B is set
len {} is Relation-like non-empty empty-yielding NAT -defined epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like one-to-one constant functional empty Function-yielding V32() ext-real non positive non negative V36() V37() finite finite-yielding V42() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered Element of NAT
B is set
f is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X
len f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
Y is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X
{ (Y ^ <*b1*>) where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT : Y ^ <*b1*> in X } is set
B is set
f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
<*f*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
Y ^ <*f*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
X is non empty Tree-like set
Y is (X)
B is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal set
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X : len b1 = B } is set
f is set
f is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
D is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
x is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X
len x is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
g is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X
len g is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
X is non empty Tree-like set
Y is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X
(X,Y) is Element of bool X
bool X is non empty set
{ (Y ^ <*b1*>) where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT : Y ^ <*b1*> in X } is set
B is set
f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
<*f*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
Y ^ <*f*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
B is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
f is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len B is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
len Y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
(len Y) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V36() V37() finite cardinal Element of NAT
D is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
<*D*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
Y ^ <*D*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
len f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
D is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
<*D*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
Y ^ <*D*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
X is non empty Tree-like set
Y is AntiChain_of_Prefixes-like AntiChain_of_Prefixes of X
B is (X)
Y /\ B is Element of bool X
bool X is non empty set
f is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
D is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
the Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X
{ the Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X} is functional non empty trivial finite V42() 1 -element set
the Element of Y /\ B is Element of Y /\ B
x is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X
g is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X
{g} is functional non empty trivial finite V42() 1 -element set
y is set
y is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
D is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X
{D} is functional non empty trivial finite V42() 1 -element set
X is non empty Tree-like set
Y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal set
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X : len b1 = Y } is set
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X : S1[b1] } is set
bool X is non empty set
X is non empty Tree-like set
f is non empty Tree-like set
Y is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X
B is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
<*B*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
Y ^ <*B*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
(X,Y) is Element of bool X
bool X is non empty set
{ (Y ^ <*b1*>) where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT : Y ^ <*b1*> in X } is set
D is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of f
x is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
<*x*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
D ^ <*x*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
(f,D) is Element of bool f
bool f is non empty set
{ (D ^ <*b1*>) where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT : D ^ <*b1*> in f } is set
X is non empty Tree-like set
(X,1) is (X)
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X : len b1 = 1 } is set
Y is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X
(X,Y) is Element of bool X
bool X is non empty set
{ (Y ^ <*b1*>) where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT : Y ^ <*b1*> in X } is set
B is set
f is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X
len f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
f . 1 is set
<*(f . 1)*> is Relation-like NAT -defined Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like set
rng f is finite Element of bool NAT
{(f . 1)} is non empty trivial finite 1 -element set
D is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
<*D*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
Y ^ <*D*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
B is set
f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
<*f*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
Y ^ <*f*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
len <*f*> is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V36() V37() finite cardinal Element of NAT
D is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X
X is non empty Tree-like set
{ (X,b1) where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT : verum } is set
union { (X,b1) where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT : verum } is set
Y is set
B is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X
len B is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
(X,(len B)) is (X)
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X : len b1 = len B } is set
Y is set
B is set
f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
(X,f) is (X)
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X : len b1 = f } is set
X is non empty finite Tree-like set
height X is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
{ (X,b1) where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT : b1 <= height X } is set
union { (X,b1) where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT : b1 <= height X } is set
Y is set
B is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X
len B is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
(X,(len B)) is finite (X)
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X : len b1 = len B } is set
Y is set
B is set
f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
(X,f) is finite (X)
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X : len b1 = f } is set
X is non empty Tree-like set
Y is (X)
B is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal set
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X : len b1 = B } is set
f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
(X,f) is (X)
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X : len b1 = f } is set
F1() is non empty set
F2() is set
{ F3(b1) where b1 is Element of F1() : b1 in F2() } is set
card { F3(b1) where b1 is Element of F1() : b1 in F2() } is epsilon-transitive epsilon-connected ordinal cardinal set
card F2() is epsilon-transitive epsilon-connected ordinal cardinal set
X is Relation-like Function-like set
dom X is set
rng X is set
Y is set
B is Element of F1()
F3(B) is set
X . B is set
F3() is finite set
F1() is non empty set
F2() is finite set
{ F4(b1) where b1 is Element of F1() : b1 in F2() } is set
card F3() is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of omega
card F2() is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of omega
card { F4(b1) where b1 is Element of F1() : b1 in F2() } is epsilon-transitive epsilon-connected ordinal cardinal set
X is non empty Tree-like set
Y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
<*Y*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
Seg Y is finite Y -element Element of bool NAT
B is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X
(X,B) is Element of bool X
bool X is non empty set
{ (B ^ <*b1*>) where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT : B ^ <*b1*> in X } is set
{ H1(b1) where b1 is ext-real V36() V37() Element of REAL : b1 in Seg Y } is set
{ (B ^ <*(b1 - 1)*>) where b1 is ext-real V36() V37() Element of REAL : b1 in Seg Y } is set
f is set
D is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
<*D*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
B ^ <*D*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
B ^ <*Y*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
D + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V36() V37() finite cardinal Element of NAT
(D + 1) - 1 is ext-real V36() V37() Element of REAL
f is finite set
card f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of omega
x is finite set
card x is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of omega
card (Seg Y) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of omega
X is non empty Tree-like set
Y is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X
(X,Y) is Element of bool X
bool X is non empty set
{ (Y ^ <*b1*>) where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT : Y ^ <*b1*> in X } is set
B is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
f is finite set
card f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of omega
X is non empty Tree-like () set
Y is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X
(X,Y) is Element of bool X
bool X is non empty set
{ (Y ^ <*b1*>) where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT : Y ^ <*b1*> in X } is set
X is non empty Tree-like set
bool X is non empty set
Y is Element of bool X
B is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
f is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
{{}} is functional non empty trivial finite V42() 1 -element Tree-like set
X is non empty Tree-like set
bool X is non empty set
Y is Element of bool X
B is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
f is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
X is non empty Tree-like set
X is non empty Tree-like set
X is non empty Tree-like set
bool X is non empty set
Y is set
B is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
ProperPrefixes B is finite set
B is set
union B is set
f is set
D is set
f is Element of bool X
D is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
x is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
g is set
y is set
D is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
x is set
ProperPrefixes D is finite set
B is set
f is (X)
D is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
ProperPrefixes D is finite set
D is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
ProperPrefixes D is finite set
{D} is functional non empty trivial finite V42() 1 -element set
(ProperPrefixes D) \/ {D} is non empty finite set
g is Element of bool X
y is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
y is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
y is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
ProperPrefixes y is finite set
y is set
y is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X
X is non empty Tree-like set
Y is (X)
the Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X
f is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
X is non empty Tree-like set
Y is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
B is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
ProperPrefixes B is finite set
f is (X)
D is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X
x is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X
X is non empty Tree-like set
Y is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
B is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
f is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
ProperPrefixes f is finite set
D is (X)
ProperPrefixes B is finite set
X is non empty Tree-like set
Y is (X)
X is non empty Tree-like set
Y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
B is finite (X)
card B is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of omega
the Element of B is Element of B
D is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X
x is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
len x is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
f + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V36() V37() finite cardinal Element of NAT
D is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
len D is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
D is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
len D is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
Seg f is finite f -element Element of bool NAT
D | (Seg f) is Relation-like NAT -defined Seg f -defined NAT -defined NAT -valued Function-like finite FinSubsequence-like Element of bool [:NAT,NAT:]
bool [:NAT,NAT:] is non empty non trivial non finite set
x is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len x is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
ProperPrefixes x is finite set
card (ProperPrefixes x) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of omega
B \ (ProperPrefixes x) is finite Element of bool X
bool X is non empty set
the Element of B \ (ProperPrefixes x) is Element of B \ (ProperPrefixes x)
y is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X
{y} is functional non empty trivial finite V42() 1 -element set
(ProperPrefixes x) \/ {y} is non empty finite set
card ((ProperPrefixes x) \/ {y}) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V36() V37() finite cardinal Element of omega
B \ ((ProperPrefixes x) \/ {y}) is finite Element of bool X
the Element of B \ ((ProperPrefixes x) \/ {y}) is Element of B \ ((ProperPrefixes x) \/ {y})
T1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X
len y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
len T1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
X is non empty Tree-like set
Y is (X)
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X : ex b2 being Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT st
( b2 in Y & b1 c= b2 ) } is set
B is set
f is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X
D is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
bool X is non empty set
B is Element of bool X
f is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
D is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
x is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X
g is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
x is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
g is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X
y is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
g is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
X is non empty Tree-like set
Y is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
B is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
f is non empty (X) (X)
ProperPrefixes B is finite set
X is non empty Tree-like set
Y is non empty (X) (X)
the Element of Y is Element of Y
f is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X
X is non empty Tree-like set
Y is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
len Y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
B is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
len B is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
f is (X)
ProperPrefixes Y is finite set
X is non empty Tree-like set
Y is (X)
bool X is non empty set
B is set
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X : ex b2 being Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT st
( b2 in Y & b1 c= b2 ) } is set
D is set
x is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X
D is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
x is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X
g is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
x is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
ProperPrefixes D is finite set
g is set
y is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
y is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X
T1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
D is set
union D is set
x is set
g is set
x is Element of bool X
g is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
y is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
y is set
T1 is set
g is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
y is set
ProperPrefixes g is finite set
the Element of D is Element of D
D is set
x is (X)
g is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
ProperPrefixes g is finite set
g is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
ProperPrefixes g is finite set
{g} is functional non empty trivial finite V42() 1 -element set
(ProperPrefixes g) \/ {g} is non empty finite set
y is Element of bool X
T1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
k1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
T1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
ProperPrefixes T1 is finite set
T1 is set
k1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X
g is non empty (X) (X)
F1() is set
X is set
Y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
Y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal set
B is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
X is set
X /\ NAT is Element of bool REAL
Y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
X /\ NAT is Element of bool REAL
Y is finite set
B is set
D is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
f is set
x is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
g is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
B is set
x is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
f is set
g is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
D is set
y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
B is set
f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
x is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
D is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
X /\ NAT is Element of bool REAL
Y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
F2() is set
F1() is set
X is set
Y is set
B is set
Y is Relation-like Function-like set
dom Y is set
B is Relation-like Function-like set
dom B is set
B . 0 is set
rng B is set
f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
B . f is set
f + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V36() V37() finite cardinal Element of NAT
B . (f + 1) is set
Y . (B . f) is set
f is set
D is set
B . D is set
x is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
B . x is set
f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
B . f is set
f + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V36() V37() finite cardinal Element of NAT
B . (f + 1) is set
Y . (B . f) is set
X is non empty Tree-like set
Y is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X
len Y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
(X,Y) is Element of bool X
bool X is non empty set
{ (Y ^ <*b1*>) where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT : Y ^ <*b1*> in X } is set
B is set
f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
<*f*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
Y ^ <*f*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
len (Y ^ <*f*>) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V36() V37() finite cardinal Element of NAT
D is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
(len (Y ^ <*f*>)) + D is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V36() V37() finite cardinal Element of NAT
g is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
x is non empty (X) (X)
y is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
len g is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
(len g) + D is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
len y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
B is Relation-like Function-like set
dom B is set
rng B is set
f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
f + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V36() V37() finite cardinal Element of NAT
(len Y) + (f + 1) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V36() V37() finite cardinal Element of NAT
D is non empty (X) (X)
x is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
len x is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
x is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
len x is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
(len Y) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V36() V37() finite cardinal Element of NAT
Seg ((len Y) + 1) is non empty finite (len Y) + 1 -element Element of bool NAT
x | (Seg ((len Y) + 1)) is Relation-like NAT -defined Seg ((len Y) + 1) -defined NAT -defined NAT -valued Function-like finite FinSubsequence-like Element of bool [:NAT,NAT:]
bool [:NAT,NAT:] is non empty non trivial non finite set
((len Y) + 1) + f is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V36() V37() finite cardinal Element of NAT
g is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
len g is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
y is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
Y ^ y is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
(len Y) + (len y) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
y . 1 is set
<*(y . 1)*> is Relation-like NAT -defined Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like set
dom g is finite Element of bool NAT
Seg (len g) is finite len g -element Element of bool NAT
1 + (len Y) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V36() V37() finite cardinal Element of NAT
Y ^ <*(y . 1)*> is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set
(Y ^ <*(y . 1)*>) . ((len Y) + 1) is set
rng g is finite Element of bool NAT
y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
<*y*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
Y ^ <*y*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
B . (Y ^ <*y*>) is set
T1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
(len g) + T1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
Y is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X
len Y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
B is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
(len Y) + B is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
B + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V36() V37() finite cardinal Element of NAT
f is finite (X)
card f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of omega
D is non empty (X) (X)
B + 0 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
x is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
len x is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
B is set
f is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X
len f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
D is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
<*D*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
f ^ <*D*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
len (f ^ <*D*>) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V36() V37() finite cardinal Element of NAT
x is set
g is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X
len g is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
(len g) + y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
B is Relation-like Function-like set
dom B is set
rng B is set
B . 0 is set
B is Relation-like Function-like set
dom B is set
rng B is set
B . 0 is set
bool X is non empty set
D is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal set
B . D is set
D + 0 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal set
B . (D + 0) is set
x is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
g is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
x is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal set
D + x is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal set
B . (D + x) is set
x + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V36() V37() finite cardinal Element of NAT
D + (x + 1) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V36() V37() finite cardinal set
B . (D + (x + 1)) is set
g is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
y is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
D + (x + 1) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V36() V37() finite cardinal Element of NAT
B . (D + (x + 1)) is set
y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
T1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
y + T1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
B . (y + T1) is set
(y + T1) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V36() V37() finite cardinal Element of NAT
B . ((y + T1) + 1) is set
k1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
T2 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
<*T2*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
k1 ^ <*T2*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
D is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
x is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
B . D is set
B . x is set
g is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
y is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal set
D + y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
f is Element of bool X
D is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
x is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
g is set
B . g is set
y is set
B . y is set
y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
T1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
D is (X)
x is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
len x is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
x is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
B . x is set
x + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V36() V37() finite cardinal Element of NAT
B . (x + 1) is set
g is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
len g is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
y is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
<*y*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
y ^ <*y*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
len y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
len <*y*> is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V36() V37() finite cardinal Element of NAT
(len y) + (len <*y*>) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V36() V37() finite cardinal Element of NAT
(len y) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V36() V37() finite cardinal Element of NAT
x is set
B . x is set
g is set
B . g is set
y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
B . y is set
y + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V36() V37() finite cardinal Element of NAT
B . (y + 1) is set
T1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
k1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
<*k1*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
T1 ^ <*k1*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
B . y is set
y + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V36() V37() finite cardinal Element of NAT
B . (y + 1) is set
len T1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
T2 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
k2 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
<*k2*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
T2 ^ <*k2*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
X is non empty Tree-like () set
Y is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of X
(X,Y) is finite Element of bool X
bool X is non empty set
{ (Y ^ <*b1*>) where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT : Y ^ <*b1*> in X } is set
the non empty Tree-like set is non empty Tree-like set
[: the non empty Tree-like set ,NAT:] is Relation-like non empty non trivial non finite set
bool [: the non empty Tree-like set ,NAT:] is non empty non trivial non finite set
the non empty Tree-like set --> 0 is Relation-like the non empty Tree-like set -defined NAT -valued Function-like constant non empty total V25( the non empty Tree-like set , NAT ) Function-yielding V32() Element of bool [: the non empty Tree-like set ,NAT:]
Y is Relation-like the non empty Tree-like set -defined NAT -valued Function-like constant non empty total V25( the non empty Tree-like set , NAT ) Function-yielding V32() Element of bool [: the non empty Tree-like set ,NAT:]
dom Y is non empty Element of bool the non empty Tree-like set
bool the non empty Tree-like set is non empty set
X is Relation-like Function-like () set
dom X is set
X is non empty set
the non empty Tree-like set is non empty Tree-like set
the Element of X is Element of X
the non empty Tree-like set --> the Element of X is Relation-like the non empty Tree-like set -defined X -valued Function-like constant non empty total V25( the non empty Tree-like set ,X) Element of bool [: the non empty Tree-like set ,X:]
[: the non empty Tree-like set ,X:] is Relation-like non empty set
bool [: the non empty Tree-like set ,X:] is non empty set
dom ( the non empty Tree-like set --> the Element of X) is non empty Element of bool the non empty Tree-like set
bool the non empty Tree-like set is non empty set
D is Relation-like Function-like () set
X is non empty set
Y is Relation-like X -valued Function-like () set
dom Y is non empty Tree-like set
B is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of dom Y
Y . B is set
rng Y is Element of bool X
bool X is non empty set
X is Relation-like Function-like () set
dom X is non empty Tree-like set
Y is Relation-like Function-like () set
dom Y is non empty Tree-like set
B is set
f is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of dom X
X . f is set
Y . f is set
X . B is set
Y . B is set
F1() is non empty Tree-like set
X is set
Y is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of F1()
B is set
X is Relation-like Function-like set
dom X is set
Y is Relation-like Function-like () set
dom Y is non empty Tree-like set
B is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
Y . B is set
F1() is non empty Tree-like set
X is Relation-like Function-like set
dom X is set
Y is Relation-like Function-like () set
dom Y is non empty Tree-like set
B is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
Y . B is set
F2(B) is set
X is Relation-like Function-like () set
dom X is non empty Tree-like set
Leaves (dom X) is Element of bool (dom X)
bool (dom X) is non empty set
X .: (Leaves (dom X)) is set
Y is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
(dom X) | Y is non empty Tree-like set
B is Relation-like Function-like () set
dom B is non empty Tree-like set
f is Relation-like Function-like () set
dom f is non empty Tree-like set
D is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
B . D is set
Y ^ D is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
X . (Y ^ D) is set
f . D is set
X is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
Y is Relation-like Function-like () set
dom Y is non empty Tree-like set
(Y,X) is Relation-like Function-like () set
rng (Y,X) is set
rng Y is set
B is set
dom (Y,X) is non empty Tree-like set
f is set
(Y,X) . f is set
(dom Y) | X is non empty Tree-like set
D is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of dom (Y,X)
X ^ D is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
Y . (X ^ D) is set
X is non empty set
Y is Relation-like X -valued Function-like () set
(Y) is set
dom Y is non empty Tree-like set
Leaves (dom Y) is Element of bool (dom Y)
bool (dom Y) is non empty set
Y .: (Leaves (dom Y)) is set
bool X is non empty set
rng Y is Element of bool X
X is non empty set
Y is Relation-like X -valued Function-like () set
dom Y is non empty Tree-like set
B is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of dom Y
(Y,B) is Relation-like Function-like () set
rng (Y,B) is set
rng Y is Element of bool X
bool X is non empty set
Y is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
X is Relation-like Function-like () set
dom X is non empty Tree-like set
B is Relation-like Function-like () set
dom B is non empty Tree-like set
(dom X) with-replacement (Y,(dom B)) is non empty Tree-like set
f is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
X . f is set
D is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
Y ^ D is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
B . D is set
{} NAT is Relation-like non-empty empty-yielding NAT -defined epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like one-to-one constant functional empty proper Function-yielding V32() ext-real non positive non negative V36() V37() finite finite-yielding V42() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered Element of bool NAT
B . ({} NAT) is set
Y ^ (<*> NAT) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
D is set
g is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
Y ^ g is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
x is set
B . g is set
f is Relation-like Function-like () set
dom f is non empty Tree-like set
D is Relation-like Function-like () set
dom D is non empty Tree-like set
x is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
f . x is set
D . x is set
X . x is set
g is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
Y ^ g is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
B . g is set
y is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
Y ^ y is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
B . y is set
X is non empty Tree-like set
Y is set
X --> Y is Relation-like X -defined {Y} -valued Function-like constant non empty total V25(X,{Y}) Element of bool [:X,{Y}:]
{Y} is non empty trivial finite 1 -element set
[:X,{Y}:] is Relation-like non empty set
bool [:X,{Y}:] is non empty set
dom (X --> Y) is non empty Element of bool X
bool X is non empty set
X is non empty set
union X is set
the Element of X is Element of X
Y is non empty Tree-like set
B is non empty set
f is set
f is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
ProperPrefixes f is finite set
D is set
x is non empty Tree-like set
f is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
D is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
<*D*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
f ^ <*D*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
x is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V36() V37() finite cardinal Element of NAT
<*x*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
f ^ <*x*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
g is set
y is non empty Tree-like set
X is set
union X is set
Y is set
B is set
f is Relation-like Function-like set
Y is set
B is set
[Y,B] is set
{Y,B} is non empty finite set
{Y} is non empty trivial finite 1 -element set
{{Y,B},{Y}} is non empty finite V42() set
f is set
[Y,f] is set
{Y,f} is non empty finite set
{{Y,f},{Y}} is non empty finite V42() set
D is set
x is set
g is Relation-like Function-like set
y is Relation-like Function-like set
X is non empty set
union X is set
Y is set
B is set
f is Relation-like Function-like () set
dom f is non empty Tree-like set
B is Relation-like Function-like set
dom B is set
rng B is set
D is set
f is non empty set
x is set
B . x is set
g is Relation-like Function-like () set
dom g is non empty Tree-like set
union f is set
Y is Relation-like Function-like set
dom Y is set
D is set
x is set
[D,x] is set
{D,x} is non empty finite set