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 epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of omega
card (Seg a) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of omega
Seg (len k) is finite len k -element Element of K40(NAT)
card (Seg (len k)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of omega
card a is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of omega
card (len k) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of omega
k is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal set
x 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
k is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal 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)
y 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 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
x is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal set
x + 1 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
m is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
len m is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
x + 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 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
a is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
k 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 Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
len x 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
card {} 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 omega
a is Relation-like NAT -defined NAT -valued Function-like finite 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
card f is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of omega
a is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal set
k is finite set
card k is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of omega
card a is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of omega
card (card f) is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of omega
a is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal set
k is finite set
card k is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of omega
k is finite set
card k is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of omega
x is set
x 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
z 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)
x is () set
z is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
y is finite () (f)
card y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of omega
x is finite () (f)
card x is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of omega
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 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
k is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
x is finite () (f)
card x is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of omega
y is finite () (f)
card y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of omega
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
card {{}} is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of omega
a is finite () (f)
card a is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of omega
((0)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
len (<*> NAT) 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
f 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
f 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
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
a is set
k is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like (f)
len k is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
a is set
f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
f + 1 is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT
((f + 1)) 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 + 1 <= 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 + 1 <= b1 } \/ {{}} is non empty set
(((f + 1))) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
<*0*> 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 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 positive non negative V16() non empty V20() finite cardinal Element of 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
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
len k is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
((0)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
a is finite () ((0))
k is finite () ((0))
card k is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of omega
x is finite () ((0))
card x is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of omega
a is finite () ((0))
card a is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of omega
f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
f + 1 is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT
((f + 1)) 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 + 1 <= 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 + 1 <= b1 } \/ {{}} is non empty set
(((f + 1))) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() 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
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
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
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
k is () set
x is finite () (((f + 1)))
y is finite () (((f + 1)))
Seg (f + 1) is non empty finite f + 1 -element Element of K40(NAT)
z is set
x is set
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
m + 1 is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT
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
m + 1 is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT
<*m*> . 1 is set
z 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 + 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
z is Relation-like Function-like set
dom z is set
rng z is set
x is set
z . x is set
x is set
z . 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
m + 1 is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT
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
m + 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
x is set
z . 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
m + 1 is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT
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
<*m*> . 1 is set
<*m*> . 1 is set
0 + 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
x is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal set
1 + m is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT
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
z . <*m*> is set
r is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
<*r*> is Relation-like NAT -defined NAT -valued non empty V18() Function-like constant finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
r + 1 is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT
card (Seg (f + 1)) is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of omega
card y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of omega
z is finite () (((f + 1)))
x is set
x is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
card {{}} is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of omega
1 + f is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT
x is set
card z is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of omega
k is finite () (((f + 1)))
card k is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of omega
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
a is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like (f)
(f,a) is non empty finite () set
((f,a)) 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 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
a ^ k is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
len (a ^ k) 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
(len a) + (len k) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
(len k) + (len a) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
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
a is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like (f)
(f,a) is non empty finite () set
((f,a)) 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
len a 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 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
a ^ k is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
len (a ^ k) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
(len a) + (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
((f,a)) + 1 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 set
a is non empty finite () set
(a) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element 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
x is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like (a)
(a,x) is non empty finite () set
((a,x)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
(a,<*k*>) is non empty () set
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
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
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 Function-like finite FinSequence-like FinSubsequence-like set
(f ^ a) ^ x is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
a ^ x is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
f ^ (a ^ x) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
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 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 Function-like finite FinSequence-like FinSubsequence-like set
<*a*> ^ k is Relation-like NAT -defined non empty Function-like finite FinSequence-like FinSubsequence-like set
(<*a*> ^ k) . 1 is set
x is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
<*f*> ^ x is Relation-like NAT -defined non empty Function-like finite FinSequence-like FinSubsequence-like set
(1) 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 1 <= 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 1 <= b1 } \/ {{}} is non empty set
<*0*> is Relation-like NAT -defined NAT -valued non empty V18() Function-like constant finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
{{},<*0*>} is non empty functional finite V37() set
f is set
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 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 Relation-like NAT -defined NAT -valued non empty V18() Function-like constant finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
(2) 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 2 <= 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 2 <= b1 } \/ {{}} is non empty set
<*1*> is Relation-like NAT -defined NAT -valued non empty V18() Function-like constant finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT
{{},<*0*>,<*1*>} is finite set
f is set
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 non empty () set
(f) is Element of K40(f)
K40(f) is set
a is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like (f)
a ^ <*0*> is Relation-like NAT -defined NAT -valued non empty Function-like finite 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 Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
a ^ x 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 a 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
(len a) + (len y) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() 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 is Relation-like NAT -defined NAT -valued Function-like finite 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
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
a ^ <*x*> is Relation-like NAT -defined NAT -valued non empty Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
(a ^ <*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
(f) is Element of K40(f)
K40(f) is set
a is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like (f)
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
a ^ <*k*> is Relation-like NAT -defined NAT -valued non empty Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
a ^ {} is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
k is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
x is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
a ^ x 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 a 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
(len a) + (len y) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() 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 is Relation-like NAT -defined NAT -valued Function-like finite 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
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
a ^ <*x*> is Relation-like NAT -defined NAT -valued non empty Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
(a ^ <*x*>) ^ z is Relation-like NAT -defined NAT -valued non empty Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
{ (b1 |-> 0) where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT : verum } is set
() is set
0 |-> 0 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 0 -element FinSequence-like FinSubsequence-like FinSequence-membered V44() V45() Element of 0 -tuples_on NAT
0 -tuples_on NAT is non empty functional FinSequence-membered FinSequenceSet of NAT
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of NAT * : len b1 = 0 } is set
Seg 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 0 -element {} -element FinSequence-like FinSubsequence-like FinSequence-membered V44() V45() Element of K40(NAT)
K166((Seg 0),0) is Relation-like non-empty empty-yielding NAT -defined Seg 0 -defined Seg 0 -defined NAT -valued {0} -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 V26( Seg 0) V26( Seg 0) V30( Seg 0,{0}) finite finite-yielding V37() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V44() V45() Element of K40(K41((Seg 0),{0}))
{0} is non empty V18() functional finite V37() 1 -element () set
K41((Seg 0),{0}) is Relation-like finite set
K40(K41((Seg 0),{0})) is finite V37() set
a is set
k is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
k |-> 0 is Relation-like empty-yielding NAT -defined NAT -valued Function-like finite k -element FinSequence-like FinSubsequence-like Element of k -tuples_on NAT
k -tuples_on NAT is non empty functional FinSequence-membered FinSequenceSet of NAT
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of NAT * : len b1 = k } is set
Seg k is finite k -element Element of K40(NAT)
K166((Seg k),0) is Relation-like NAT -defined Seg k -defined Seg k -defined NAT -valued {0} -valued Function-like constant V26( Seg k) V26( Seg k) V30( Seg k,{0}) finite FinSequence-like FinSubsequence-like V44() V45() Element of K40(K41((Seg k),{0}))
K41((Seg k),{0}) is Relation-like finite set
K40(K41((Seg k),{0})) is finite V37() set
a is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
(a) is finite set
k is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
k |-> 0 is Relation-like empty-yielding NAT -defined NAT -valued Function-like finite k -element FinSequence-like FinSubsequence-like Element of k -tuples_on NAT
k -tuples_on NAT is non empty functional FinSequence-membered FinSequenceSet of NAT
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of NAT * : len b1 = k } is set
Seg k is finite k -element Element of K40(NAT)
K166((Seg k),0) is Relation-like NAT -defined Seg k -defined Seg k -defined NAT -valued {0} -valued Function-like constant V26( Seg k) V26( Seg k) V30( Seg k,{0}) finite FinSequence-like FinSubsequence-like V44() V45() Element of K40(K41((Seg k),{0}))
K41((Seg k),{0}) is Relation-like finite set
K40(K41((Seg k),{0})) is finite V37() set
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) |-> 0 is Relation-like empty-yielding NAT -defined NAT -valued Function-like finite len y -element FinSequence-like FinSubsequence-like Element of (len y) -tuples_on NAT
(len y) -tuples_on NAT is non empty functional FinSequence-membered FinSequenceSet of NAT
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of NAT * : len b1 = len y } is set
Seg (len y) is finite len y -element Element of K40(NAT)
K166((Seg (len y)),0) is Relation-like NAT -defined Seg (len y) -defined Seg (len y) -defined NAT -valued {0} -valued Function-like constant V26( Seg (len y)) V26( Seg (len y)) V30( Seg (len y),{0}) finite FinSequence-like FinSubsequence-like V44() V45() Element of K40(K41((Seg (len y)),{0}))
K41((Seg (len y)),{0}) is Relation-like finite set
K40(K41((Seg (len y)),{0})) is finite V37() set
z is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal set
y . z is set
((len y) |-> 0) . z 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
dom y is finite Element of K40(NAT)
a . z is set
len ((len y) |-> 0) 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 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
a ^ <*k*> 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
a ^ <*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 |-> 0 is Relation-like empty-yielding NAT -defined NAT -valued Function-like finite y -element FinSequence-like FinSubsequence-like Element of y -tuples_on NAT
y -tuples_on NAT is non empty functional FinSequence-membered FinSequenceSet of NAT
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of NAT * : len b1 = y } is set
Seg y is finite y -element Element of K40(NAT)
K166((Seg y),0) is Relation-like NAT -defined Seg y -defined Seg y -defined NAT -valued {0} -valued Function-like constant V26( Seg y) V26( Seg y) V30( Seg y,{0}) finite FinSequence-like FinSubsequence-like V44() V45() Element of K40(K41((Seg y),{0}))
K41((Seg y),{0}) is Relation-like finite set
K40(K41((Seg y),{0})) is finite V37() set
len (a ^ <*k*>) 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 a) + 1 is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT
(a ^ <*k*>) . (len (a ^ <*k*>)) is set
len (a ^ <*x*>) is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT
(len (a ^ <*x*>)) |-> 0 is Relation-like empty-yielding NAT -defined NAT -valued Function-like finite len (a ^ <*x*>) -element FinSequence-like FinSubsequence-like Element of (len (a ^ <*x*>)) -tuples_on NAT
(len (a ^ <*x*>)) -tuples_on NAT is non empty functional FinSequence-membered FinSequenceSet of NAT
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of NAT * : len b1 = len (a ^ <*x*>) } is set
Seg (len (a ^ <*x*>)) is non empty finite len (a ^ <*x*>) -element Element of K40(NAT)
K166((Seg (len (a ^ <*x*>))),0) is Relation-like NAT -defined Seg (len (a ^ <*x*>)) -defined Seg (len (a ^ <*x*>)) -defined NAT -valued {0} -valued non empty Function-like constant V26( Seg (len (a ^ <*x*>))) V26( Seg (len (a ^ <*x*>))) V30( Seg (len (a ^ <*x*>)),{0}) finite FinSequence-like FinSubsequence-like V44() V45() Element of K40(K41((Seg (len (a ^ <*x*>))),{0}))
K41((Seg (len (a ^ <*x*>))),{0}) is Relation-like finite set
K40(K41((Seg (len (a ^ <*x*>))),{0})) is finite V37() set
z is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal set
((len (a ^ <*x*>)) |-> 0) . z 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
(a ^ <*x*>) . z is set
(a ^ <*k*>) . z is set
len ((len (a ^ <*x*>)) |-> 0) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() 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 |-> 0 is Relation-like empty-yielding NAT -defined NAT -valued Function-like finite f -element FinSequence-like FinSubsequence-like Element of f -tuples_on NAT
f -tuples_on NAT is non empty functional FinSequence-membered FinSequenceSet of NAT
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of NAT * : len b1 = f } is set
Seg f is finite f -element Element of K40(NAT)
K166((Seg f),0) is Relation-like NAT -defined Seg f -defined Seg f -defined NAT -valued {0} -valued Function-like constant V26( Seg f) V26( Seg f) V30( Seg f,{0}) finite FinSequence-like FinSubsequence-like V44() V45() Element of K40(K41((Seg f),{0}))
{0} is non empty V18() functional finite V37() 1 -element () set
K41((Seg f),{0}) is Relation-like finite set
K40(K41((Seg f),{0})) is finite V37() set
a is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like (())
K41(NAT,()) is Relation-like V18() non finite set
K40(K41(NAT,())) is V18() non finite set
f is Relation-like NAT -defined () -valued Function-like V30( NAT ,()) Element of K40(K41(NAT,()))
dom f is set
rng f is set
a is set
k is set
f . a is set
f . k is set
x is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
f . x is Element of ()
x |-> 0 is Relation-like empty-yielding NAT -defined NAT -valued Function-like finite x -element FinSequence-like FinSubsequence-like Element of x -tuples_on NAT
x -tuples_on NAT is non empty functional FinSequence-membered FinSequenceSet of NAT
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of NAT * : len b1 = x } is set
Seg x is finite x -element Element of K40(NAT)
K166((Seg x),0) is Relation-like NAT -defined Seg x -defined Seg x -defined NAT -valued {0} -valued Function-like constant V26( Seg x) V26( Seg x) V30( Seg x,{0}) finite FinSequence-like FinSubsequence-like V44() V45() Element of K40(K41((Seg x),{0}))
{0} is non empty V18() functional finite V37() 1 -element () set
K41((Seg x),{0}) is Relation-like finite set
K40(K41((Seg x),{0})) is finite V37() set
y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
f . y is Element of ()
y |-> 0 is Relation-like empty-yielding NAT -defined NAT -valued Function-like finite y -element FinSequence-like FinSubsequence-like Element of y -tuples_on NAT
y -tuples_on NAT is non empty functional FinSequence-membered FinSequenceSet of NAT
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of NAT * : len b1 = y } is set
Seg y is finite y -element Element of K40(NAT)
K166((Seg y),0) is Relation-like NAT -defined Seg y -defined Seg y -defined NAT -valued {0} -valued Function-like constant V26( Seg y) V26( Seg y) V30( Seg y,{0}) finite FinSequence-like FinSubsequence-like V44() V45() Element of K40(K41((Seg y),{0}))
K41((Seg y),{0}) is Relation-like finite set
K40(K41((Seg y),{0})) is finite V37() set
a is set
k is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT
k |-> 0 is Relation-like empty-yielding NAT -defined NAT -valued Function-like finite k -element FinSequence-like FinSubsequence-like Element of k -tuples_on NAT
k -tuples_on NAT is non empty functional FinSequence-membered FinSequenceSet of NAT
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of NAT * : len b1 = k } is set
Seg k is finite k -element Element of K40(NAT)
K166((Seg k),0) is Relation-like NAT -defined Seg k -defined Seg k -defined NAT -valued {0} -valued Function-like constant V26( Seg k) V26( Seg k) V30( Seg k,{0}) finite FinSequence-like FinSubsequence-like V44() V45() Element of K40(K41((Seg k),{0}))
{0} is non empty V18() functional finite V37() 1 -element () set
K41((Seg k),{0}) is Relation-like finite set
K40(K41((Seg k),{0})) is finite V37() set
f . k is Element of ()