:: TREES_1 semantic presentation

REAL is set
NAT is epsilon-transitive epsilon-connected ordinal non empty V18() non finite cardinal limit_cardinal Element of K40(REAL)
K40(REAL) is set
omega is epsilon-transitive epsilon-connected ordinal non empty V18() non finite cardinal limit_cardinal set
K40(omega) is V18() non finite set
K40(NAT) is V18() non finite set
{} is Relation-like non-empty empty-yielding NAT -defined epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural ext-real non positive non negative V16() empty V20() Function-like one-to-one constant functional finite finite-yielding V37() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V44() V45() set
the Relation-like non-empty empty-yielding NAT -defined epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural ext-real non positive non negative V16() empty V20() Function-like one-to-one constant functional finite finite-yielding V37() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V44() V45() set is Relation-like non-empty empty-yielding NAT -defined epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural ext-real non positive non negative V16() empty V20() Function-like one-to-one constant functional finite finite-yielding V37() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V44() V45() set
1 is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT
2 is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT
3 is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() 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 ext-real non positive non negative V16() empty V20() Function-like one-to-one constant functional finite finite-yielding V37() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V44() V45() Element of NAT
Seg 1 is non empty V18() finite 1 -element Element of K40(NAT)
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
dom D is finite Element of K40(NAT)
a is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal set
Seg a is finite a -element Element of K40(NAT)
k is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
Seg k is finite k -element Element of K40(NAT)
f | (Seg k) is Relation-like NAT -defined Seg k -defined NAT -defined Function-like finite FinSubsequence-like set
a is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
Seg a is finite a -element Element of K40(NAT)
f | (Seg a) is Relation-like NAT -defined Seg a -defined NAT -defined Function-like finite FinSubsequence-like set
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
a is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
Seg a is finite a -element Element of K40(NAT)
f | (Seg a) is Relation-like NAT -defined Seg a -defined NAT -defined Function-like finite FinSubsequence-like set
a is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
D ^ a is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
dom D is finite Element of K40(NAT)
len D is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
Seg (len D) is finite len D -element Element of K40(NAT)
f | (dom D) is Relation-like NAT -defined dom D -defined NAT -defined Function-like finite FinSubsequence-like set
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
len D is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
len f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
a is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
D ^ a is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len a is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
(len D) + (len a) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
D is set
<*D*> is Relation-like NAT -defined non empty V18() Function-like constant finite 1 -element FinSequence-like FinSubsequence-like set
f is set
<*f*> is Relation-like NAT -defined non empty V18() Function-like constant finite 1 -element FinSequence-like FinSubsequence-like set
len <*D*> is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT
len <*f*> is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT
<*D*> . 1 is set
D is finite set
f is finite set
card D is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of omega
card f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of omega
f \ D is finite Element of K40(f)
K40(f) is finite V37() set
card (f \ D) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of omega
(card f) - (card D) is ext-real V16() V20() set
D is finite set
f is finite set
card D is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of omega
card f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of omega
D is set
<*D*> is Relation-like NAT -defined non empty V18() Function-like constant finite 1 -element FinSequence-like FinSubsequence-like set
f is set
<*f*> is Relation-like NAT -defined non empty V18() Function-like constant finite 1 -element FinSequence-like FinSubsequence-like set
len <*D*> is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT
len <*f*> is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT
<*D*> . 1 is set
D is finite set
f is finite set
card f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of omega
card D is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of omega
D is set
<*D*> is Relation-like NAT -defined non empty V18() Function-like constant finite 1 -element FinSequence-like FinSubsequence-like set
f is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
f ^ <*D*> is Relation-like NAT -defined non empty Function-like finite FinSequence-like FinSubsequence-like set
a is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
k is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
(f ^ <*D*>) ^ k is Relation-like NAT -defined non empty Function-like finite FinSequence-like FinSubsequence-like set
<*D*> ^ k is Relation-like NAT -defined non empty Function-like finite FinSequence-like FinSubsequence-like set
f ^ (<*D*> ^ k) is Relation-like NAT -defined non empty Function-like finite FinSequence-like FinSubsequence-like set
len f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
len (f ^ <*D*>) is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT
len k is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
(len (f ^ <*D*>)) + (len k) is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT
len <*D*> is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT
(len f) + (len <*D*>) is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT
((len f) + (len <*D*>)) + (len k) is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT
(len f) + 1 is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT
((len f) + 1) + (len k) is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT
D is set
<*D*> is Relation-like NAT -defined non empty V18() Function-like constant finite 1 -element FinSequence-like FinSubsequence-like set
f is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
a is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
a ^ <*D*> is Relation-like NAT -defined non empty Function-like finite FinSequence-like FinSubsequence-like set
k is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
f ^ k is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
k ^ <*D*> is Relation-like NAT -defined non empty Function-like finite FinSequence-like FinSubsequence-like set
f ^ (k ^ <*D*>) is Relation-like NAT -defined non empty Function-like finite FinSequence-like FinSubsequence-like set
len a is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
len (a ^ <*D*>) is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT
len k is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
(len (a ^ <*D*>)) + (len k) is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT
len <*D*> is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT
(len a) + (len <*D*>) is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT
((len a) + (len <*D*>)) + (len k) is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT
(len a) + 1 is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT
((len a) + 1) + (len k) is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT
D is set
<*D*> is Relation-like NAT -defined non empty V18() Function-like constant finite 1 -element FinSequence-like FinSubsequence-like set
f is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
a is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
a ^ <*D*> is Relation-like NAT -defined non empty Function-like finite FinSequence-like FinSubsequence-like set
len f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
len (a ^ <*D*>) is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT
len a is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
len <*D*> is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT
(len a) + (len <*D*>) is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT
(len a) + 1 is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT
k is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
f ^ k is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
k is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
f ^ k 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
f is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
f ^ D is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
len D is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
(len f) + (len D) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
D is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
rng D is finite set
(rng D) * is non empty functional FinSequence-membered FinSequenceSet of rng D
a is set
k is set
x is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
rng x is finite set
y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
Seg y is finite y -element Element of K40(NAT)
D | (Seg y) is Relation-like NAT -defined Seg y -defined NAT -defined Function-like finite FinSubsequence-like set
y is Relation-like NAT -defined rng D -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of rng D
f is set
a is set
k is set
x is set
y is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
k is set
x is set
y is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
D is set
f is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
(f) is set
a 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
f is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
(f) is set
a 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
f is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
(f) is set
len f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
len D is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
f is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
a is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
f ^ a 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
(D) is set
({}) is set
the Element of ({}) is Element of ({})
f is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
{{}} is non empty V18() functional finite V37() 1 -element set
f is set
<*f*> is Relation-like NAT -defined non empty V18() Function-like constant finite 1 -element FinSequence-like FinSubsequence-like set
(<*f*>) is set
a is set
k is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len <*f*> is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT
len k is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
0 + 1 is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT
a is set
f is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
a is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
(f) is set
(a) is set
k is set
x is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
a 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
(f) is set
k 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
x is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
Seg x is finite x -element Element of K40(NAT)
f | (Seg x) is Relation-like NAT -defined Seg x -defined NAT -defined Function-like finite FinSubsequence-like set
y is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
Seg y is finite y -element Element of K40(NAT)
f | (Seg y) is Relation-like NAT -defined Seg y -defined NAT -defined Function-like finite FinSubsequence-like set
k | (Seg x) is Relation-like NAT -defined Seg x -defined NAT -defined Function-like finite FinSubsequence-like set
a | (Seg y) is Relation-like NAT -defined Seg y -defined NAT -defined Function-like finite FinSubsequence-like set
NAT * is non empty functional FinSequence-membered FinSequenceSet of NAT
f is set
f is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
(f) is set
f is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
a is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
<*a*> is Relation-like NAT -defined NAT -valued non empty V18() Function-like constant finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
f ^ <*a*> is Relation-like NAT -defined NAT -valued non empty Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
k is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
<*k*> is Relation-like NAT -defined NAT -valued non empty V18() Function-like constant finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
f ^ <*k*> is Relation-like NAT -defined NAT -valued non empty Function-like finite FinSequence-like FinSubsequence-like FinSequence 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 ext-real non positive non negative V16() empty V20() Function-like one-to-one constant functional finite finite-yielding V37() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V44() V45() FinSequence of NAT
{(<*> NAT)} is non empty V18() functional finite V37() 1 -element set
f is non empty V18() functional finite V37() 1 -element set
f is set
a is non empty () set
f is non empty () set
a is Element of f
f is non empty () set
a is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
k 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 (f)
(x) is set
(a) is set
f is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
a is non empty () set
k is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
f ^ k 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 FinSequence of NAT
len f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
Seg (len f) is finite len f -element Element of K40(NAT)
x | (Seg (len f)) is Relation-like NAT -defined Seg (len f) -defined NAT -defined NAT -valued Function-like finite FinSubsequence-like set
len x is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
len k is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
(len f) + (len k) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
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 V16() V20() finite cardinal Element of NAT
z is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal set
dom f is finite Element of K40(NAT)
x . z is set
f . z is set
y . z is set
(x) is set
<*> NAT is Relation-like non-empty empty-yielding NAT -defined NAT -valued epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural ext-real non positive non negative V16() empty V20() Function-like one-to-one constant functional finite finite-yielding V37() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V44() V45() FinSequence of NAT
f is non empty () set
the Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like (f) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like (f)
a is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
{} ^ a is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
f is non empty () set
a is non empty () set
f \/ a is non empty set
x is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
(x) is set
x 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 V16() V20() finite cardinal Element of NAT
<*y*> is Relation-like NAT -defined NAT -valued non empty V18() Function-like constant finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
x ^ <*y*> is Relation-like NAT -defined NAT -valued non empty Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
z is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
<*z*> is Relation-like NAT -defined NAT -valued non empty V18() Function-like constant finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
x ^ <*z*> is Relation-like NAT -defined NAT -valued non empty Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
f /\ a is set
x is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
(x) is set
x 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 V16() V20() finite cardinal Element of NAT
<*y*> is Relation-like NAT -defined NAT -valued non empty V18() Function-like constant finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
x ^ <*y*> is Relation-like NAT -defined NAT -valued non empty Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
z is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
<*z*> is Relation-like NAT -defined NAT -valued non empty V18() Function-like constant finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
x ^ <*z*> is Relation-like NAT -defined NAT -valued non empty Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
f is non empty () set
a is non empty () set
f \/ a is non empty () set
f is non empty () set
a is non empty () set
f /\ a is non empty () set
f is non empty finite () set
a is non empty finite () set
f \/ a is non empty finite () set
a is non empty finite () set
f is non empty () set
a /\ f is non empty finite () set
f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
{ <*b1*> where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT : not f <= b1 } is set
{ <*b1*> where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT : not f <= b1 } \/ {{}} is non empty set
k is set
x is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
<*x*> is Relation-like NAT -defined NAT -valued non empty V18() Function-like constant finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
k is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
(k) is set
x is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
<*x*> is Relation-like NAT -defined NAT -valued non empty V18() Function-like constant finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
k 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 V16() V20() finite cardinal Element of NAT
<*x*> is Relation-like NAT -defined NAT -valued non empty V18() Function-like constant finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
k ^ <*x*> is Relation-like NAT -defined NAT -valued non empty Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
<*y*> is Relation-like NAT -defined NAT -valued non empty V18() Function-like constant finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
k ^ <*y*> is Relation-like NAT -defined NAT -valued non empty Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
z is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
<*z*> is Relation-like NAT -defined NAT -valued non empty V18() Function-like constant finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
len k is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
len <*x*> is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT
(len k) + (len <*x*>) is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT
len <*z*> is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT
(len k) + 1 is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT
0 + 1 is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT
<*x*> . 1 is set
f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
(f) is non empty () set
{ <*b1*> where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT : not f <= b1 } is set
{ <*b1*> where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT : not f <= b1 } \/ {{}} is non empty set
f + 1 is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT
Seg (f + 1) is non empty finite f + 1 -element Element of K40(NAT)
k is set
x is set
y is set
z is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
<*z*> is Relation-like NAT -defined NAT -valued non empty V18() Function-like constant finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
z + 2 is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT
x is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
<*x*> is Relation-like NAT -defined NAT -valued non empty V18() Function-like constant finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
x + 2 is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT
<*z*> . 1 is set
z is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
<*z*> is Relation-like NAT -defined NAT -valued non empty V18() Function-like constant finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
z + 2 is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT
x is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
<*x*> is Relation-like NAT -defined NAT -valued non empty V18() Function-like constant finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
x + 2 is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT
k is set
x is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
<*x*> is Relation-like NAT -defined NAT -valued non empty V18() Function-like constant finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
x + 2 is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT
y is set
z is set
x is set
y is set
x is set
z is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
<*z*> is Relation-like NAT -defined NAT -valued non empty V18() Function-like constant finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
y is set
z + 2 is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT
x is set
m is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
<*m*> is Relation-like NAT -defined NAT -valued non empty V18() Function-like constant finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
x is set
m + 2 is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT
k is Relation-like Function-like set
dom k is set
rng k is set
x is set
k . x is set
y is set
k . y is set
z is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
<*z*> is Relation-like NAT -defined NAT -valued non empty V18() Function-like constant finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
z + 2 is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT
0 + 1 is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT
z + 1 is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT
(z + 1) + 1 is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT
z is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
<*z*> is Relation-like NAT -defined NAT -valued non empty V18() Function-like constant finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
z + 2 is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT
z + 1 is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT
(z + 1) + 1 is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT
z is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
<*z*> is Relation-like NAT -defined NAT -valued non empty V18() Function-like constant finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
z + 2 is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT
x is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
<*x*> is Relation-like NAT -defined NAT -valued non empty V18() Function-like constant finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
x + 2 is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT
x is set
y is set
k . y is set
1 + f is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT
z is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
<*z*> is Relation-like NAT -defined NAT -valued non empty V18() Function-like constant finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
z + 2 is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT
x is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
<*x*> is Relation-like NAT -defined NAT -valued non empty V18() Function-like constant finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
<*z*> . 1 is set
<*x*> . 1 is set
z + 1 is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT
1 + 0 is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT
(z + 1) + 1 is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT
x is set
y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
k . {} is set
z is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
<*z*> is Relation-like NAT -defined NAT -valued non empty V18() Function-like constant finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
z + 2 is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT
1 + 1 is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT
z is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal set
2 + z is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT
x is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
(1 + 1) + x is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT
1 + x is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT
1 + (1 + x) is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT
<*x*> is Relation-like NAT -defined NAT -valued non empty V18() Function-like constant finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
k . <*x*> is set
x is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
<*x*> is Relation-like NAT -defined NAT -valued non empty V18() Function-like constant finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
x + 2 is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT
f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
<*f*> is Relation-like NAT -defined NAT -valued non empty V18() Function-like constant finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
a is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
(a) is non empty finite () set
{ <*b1*> where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT : not a <= b1 } is set
{ <*b1*> where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT : not a <= b1 } \/ {{}} is non empty set
(0) is non empty finite () set
{ <*b1*> where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT : not 0 <= b1 } is set
{ <*b1*> where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT : not 0 <= b1 } \/ {{}} is non empty set
the Element of { <*b1*> where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT : not 0 <= b1 } is Element of { <*b1*> where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT : not 0 <= b1 }
a is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
<*a*> is Relation-like NAT -defined NAT -valued non empty V18() Function-like constant finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
(f) is non empty finite () set
{ <*b1*> where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT : not f <= b1 } is set
{ <*b1*> where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT : not f <= b1 } \/ {{}} is non empty set
a is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
k is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
<*k*> is Relation-like NAT -defined NAT -valued non empty V18() Function-like constant finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
f is non empty () set
K40(f) is set
a is set
k is set
k is Element of K40(f)
x 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
z is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
a is Element of K40(f)
k is Element of K40(f)
x is set
y is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
z 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
z is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
a is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
k is set
x is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
a ^ x is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
x is non empty set
y is set
y is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
(y) is set
z is set
x is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
m is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
Seg m is finite m -element Element of K40(NAT)
y | (Seg m) is Relation-like NAT -defined Seg m -defined NAT -defined NAT -valued Function-like finite FinSubsequence-like set
x is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
m is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
Seg m is finite m -element Element of K40(NAT)
y | (Seg m) is Relation-like NAT -defined Seg m -defined NAT -defined NAT -valued Function-like finite FinSubsequence-like set
m is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
x ^ m is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
a ^ y is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
a ^ x is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
(a ^ x) ^ m is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
m is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
a ^ m 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
z is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
<*z*> is Relation-like NAT -defined NAT -valued non empty V18() Function-like constant finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
y ^ <*z*> is Relation-like NAT -defined NAT -valued non empty Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
x is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
a ^ (y ^ <*z*>) is Relation-like NAT -defined NAT -valued non empty Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
a ^ y is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
(a ^ y) ^ <*z*> is Relation-like NAT -defined NAT -valued non empty Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
<*x*> is Relation-like NAT -defined NAT -valued non empty V18() Function-like constant finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
(a ^ y) ^ <*x*> is Relation-like NAT -defined NAT -valued non empty Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
y ^ <*x*> is Relation-like NAT -defined NAT -valued non empty 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
a ^ x is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
y is non empty () set
z is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
a ^ z 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
a ^ x is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
k is non empty () set
x is non empty () set
y is set
z is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
a ^ z is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
z is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
a ^ z is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
f is non empty () set
(f,(<*> NAT)) is non empty () set
a is set
k is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like ((f,(<*> NAT)))
{} ^ k is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
a is set
k is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like (f)
{} ^ k is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
f is non empty finite () set
a is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like (f)
(f,a) is non empty () set
k is Relation-like Function-like set
rng k is set
dom k is set
x is set
k . x is set
y is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
z is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
a ^ z 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
z is set
x is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
a ^ x 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 set
rng x is set
y is set
z is set
x . z is set
k . z is set
x is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
a ^ (<*> NAT) 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
a ^ x is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
y is set
z is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
a ^ z is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
x is set
k . x is set
x . x is set
x is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
m is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
a ^ m is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
f is non empty () set
(f) is Element of K40(f)
K40(f) is set
the Element of (f) is Element of (f)
k is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like (f)
f is non empty () set
the Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like (f) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like (f)
(f, the Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like (f)) is non empty () set
a is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
f is non empty () set
k is non empty () set
x is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like (f)
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like (f) : not a c< b1 } is set
{ (a ^ b1) where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like (k) : b1 = b1 } is set
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like (f) : not a c< b1 } \/ { (a ^ b1) where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like (k) : b1 = b1 } is set
z is set
x is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like (f)
x is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like (f)
y is non empty set
z is set
x is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like (k)
a ^ x is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
z is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
(z) is set
x is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like (f)
x is set
x is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
m is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like (f)
m is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like (f)
x is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like (k)
a ^ x is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
x is set
m is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
m is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
m ^ m is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len a is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
len m is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
r is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
a ^ r is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
r ^ m is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
a ^ (r ^ m) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
dom r is finite Element of K40(NAT)
len r is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
Seg (len r) is finite len r -element Element of K40(NAT)
x | (dom r) is Relation-like NAT -defined dom r -defined NAT -defined NAT -valued Function-like finite FinSubsequence-like set
t is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
r2 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like (k)
a ^ r2 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
dom m is finite Element of K40(NAT)
a | (dom m) is Relation-like NAT -defined dom m -defined NAT -defined NAT -valued Function-like finite FinSubsequence-like set
r is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
m ^ r is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
Seg (len m) is finite len m -element Element of K40(NAT)
r is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
t is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like (f)
z 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 V16() V20() finite cardinal Element of NAT
<*x*> is Relation-like NAT -defined NAT -valued non empty V18() Function-like constant finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
z ^ <*x*> is Relation-like NAT -defined NAT -valued non empty Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
x is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
<*x*> is Relation-like NAT -defined NAT -valued non empty V18() Function-like constant finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
z ^ <*x*> is Relation-like NAT -defined NAT -valued non empty Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
m is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like (f)
m is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like (f)
m is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like (f)
m is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like (k)
a ^ m is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
len z is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
len a is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
m is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
z ^ m is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
m ^ m is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
z ^ (m ^ m) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
r is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like (f)
len <*x*> is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT
(len z) + (len <*x*>) is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT
(len z) + 1 is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT
len <*x*> is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT
(len z) + (len <*x*>) is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT
len r is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
{} ^ m is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
{} ^ <*x*> is Relation-like NAT -defined non empty Function-like finite {} + 1 -element FinSequence-like FinSubsequence-like set
{} + 1 is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT
r is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like (k)
a ^ r is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
m is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
a ^ m is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
m ^ <*x*> is Relation-like NAT -defined non empty Function-like finite FinSequence-like FinSubsequence-like set
a ^ (m ^ <*x*>) is Relation-like NAT -defined non empty Function-like finite FinSequence-like FinSubsequence-like set
dom m is finite Element of K40(NAT)
len m is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
Seg (len m) is finite len m -element Element of K40(NAT)
m | (dom m) is Relation-like NAT -defined dom m -defined NAT -defined NAT -valued Function-like finite FinSubsequence-like set
r is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
r ^ <*x*> is Relation-like NAT -defined NAT -valued non empty Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
t is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like (k)
a ^ t is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
z is non empty () set
x 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 (f)
x is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like (k)
a ^ x 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
a ^ x is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
m is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
a ^ m 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
a ^ x 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
a ^ x is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
x is non empty () set
y is non empty () set
z is set
x 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
a ^ x is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
z is set
x 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
a ^ 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
a is non empty () set
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like (a) : not f c< b1 } is set
k is non empty () set
(a,f,k) is non empty () set
{ (f ^ b1) where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like (k) : b1 = b1 } is set
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like (a) : not f c< b1 } \/ { (f ^ b1) where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like (k) : b1 = b1 } is set
x is set
y is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
z is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
f ^ z is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
x is set
y is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like (k)
f ^ 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 (a)
f is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
a is non empty () set
k is non empty () set
(a,f,k) is non empty () set
((a,f,k),f) is non empty () set
x is set
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
x is set
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
f ^ {} is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
z is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
f ^ z is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
f is non empty finite () set
a is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like (f)
k is non empty finite () set
(f,a,k) is non empty () set
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like (f) : not a c< b1 } is set
x is set
y is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like (f)
{ (a ^ b1) where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like (k) : b1 = b1 } is set
x is set
y is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
a ^ 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 set
rng x is set
y is set
x . y is set
z is set
x . z is set
x is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
a ^ x 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
a ^ x is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
y is set
z is set
x . z is set
x is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
a ^ x 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 (k)
a ^ x is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
y is set
z is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like (k)
a ^ z is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
x . z is set
x is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
a ^ x is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like (f) : not a c< b1 } \/ { (a ^ b1) where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like (k) : b1 = b1 } is set
f is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
(f) is set
dom f is finite Element of K40(NAT)
a is set
k is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len k is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
(len k) + 1 is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT
x is set
a is Relation-like Function-like set
dom a is set
rng a is set
k is set
a . k is set
x is set
a . x is set
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 V16() V20() finite cardinal Element of NAT
(len y) + 1 is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT
z is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len z is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
(len z) + 1 is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT
k is set
x is set
a . x is set
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 V16() V20() finite cardinal Element of NAT
(len y) + 1 is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT
len f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
0 + 1 is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT
Seg (len f) is finite len f -element Element of K40(NAT)
k is set
len f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
Seg (len f) is finite len f -element Element of K40(NAT)
x is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal set
1 + y is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT
z is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
Seg z is finite z -element Element of K40(NAT)
f | (Seg z) is Relation-like NAT -defined Seg z -defined NAT -defined Function-like finite FinSubsequence-like 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 V16() V20() finite cardinal Element of NAT
a . x is 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 V16() V20() finite cardinal Element of NAT
(len x) + 1 is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT
f is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
(f) is set
dom f is finite Element of K40(NAT)
f is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
(f) is finite set
card (f) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of omega
len f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
dom f is finite Element of K40(NAT)
Seg (len f) is finite len f -element Element of K40(NAT)
card (dom f) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of omega
card (len f) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of omega
f is set
f is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
a 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
{f} is non empty V18() functional finite V37() 1 -element set
a is set
a is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
k 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
a is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
{f,a} is non empty functional finite V37() set
k is set
k 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
f is non empty () set
the Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like (f) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like (f)
{ the Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like (f)} is non empty V18() functional finite V37() 1 -element set
k is () set
x is set
f is non empty () set
a is set
a is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
k is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
a is () set
k is () set
x is set
f is non empty () set
a is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like (f)
{a} is non empty V18() functional finite V37() 1 -element set
k is () set
x is set
f is non empty () set
a is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like (f)
k is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like (f)
{a,k} is non empty functional finite V37() set
x is () set
y is set
f is non empty finite () set
a is () (f)
f is non empty finite () set
a is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal set
Seg a is finite a -element Element of K40(NAT)
k is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
len k is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
(k) is finite set
dom k is finite Element of K40(NAT)
card (k) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of omega
card f is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of omega
card (dom k) is