:: TREES_1 semantic presentation

REAL is set

NAT is epsilon-transitive epsilon-connected ordinal non empty V18() non finite cardinal limit_cardinal Element of K40(REAL)

K40(REAL) is set

omega is epsilon-transitive epsilon-connected ordinal non empty V18() non finite cardinal limit_cardinal set

K40(omega) is V18() non finite set

K40(NAT) is V18() non finite set

{} is Relation-like non-empty empty-yielding NAT -defined epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural ext-real non positive non negative V16() empty V20() Function-like one-to-one constant functional finite finite-yielding V37() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V44() V45() set

the Relation-like non-empty empty-yielding NAT -defined epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural ext-real non positive non negative V16() empty V20() Function-like one-to-one constant functional finite finite-yielding V37() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V44() V45() set is Relation-like non-empty empty-yielding NAT -defined epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural ext-real non positive non negative V16() empty V20() Function-like one-to-one constant functional finite finite-yielding V37() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V44() V45() set

1 is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT

2 is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT

3 is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT

0 is Relation-like non-empty empty-yielding NAT -defined epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural ext-real non positive non negative V16() empty V20() Function-like one-to-one constant functional finite finite-yielding V37() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V44() V45() Element of NAT

Seg 1 is non empty V18() finite 1 -element Element of K40(NAT)

D is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

f is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

dom D is finite Element of K40(NAT)

a is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal set

Seg a is finite a -element Element of K40(NAT)

k is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT

Seg k is finite k -element Element of K40(NAT)

f | (Seg k) is Relation-like NAT -defined Seg k -defined NAT -defined Function-like finite FinSubsequence-like set

a is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT

Seg a is finite a -element Element of K40(NAT)

f | (Seg a) is Relation-like NAT -defined Seg a -defined NAT -defined Function-like finite FinSubsequence-like set

D is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

f is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

a is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT

Seg a is finite a -element Element of K40(NAT)

f | (Seg a) is Relation-like NAT -defined Seg a -defined NAT -defined Function-like finite FinSubsequence-like set

a is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

D ^ a is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

dom D is finite Element of K40(NAT)

len D is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT

Seg (len D) is finite len D -element Element of K40(NAT)

f | (dom D) is Relation-like NAT -defined dom D -defined NAT -defined Function-like finite FinSubsequence-like set

D is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

f is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

len D is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT

len f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT

a is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

D ^ a is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

len a is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT

(len D) + (len a) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT

D is set

<*D*> is Relation-like NAT -defined non empty V18() Function-like constant finite 1 -element FinSequence-like FinSubsequence-like set

f is set

<*f*> is Relation-like NAT -defined non empty V18() Function-like constant finite 1 -element FinSequence-like FinSubsequence-like set

len <*D*> is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT

len <*f*> is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT

<*D*> . 1 is set

D is finite set

f is finite set

card D is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of omega

card f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of omega

f \ D is finite Element of K40(f)

K40(f) is finite V37() set

card (f \ D) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of omega

(card f) - (card D) is ext-real V16() V20() set

D is finite set

f is finite set

card D is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of omega

card f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of omega

D is set

<*D*> is Relation-like NAT -defined non empty V18() Function-like constant finite 1 -element FinSequence-like FinSubsequence-like set

f is set

<*f*> is Relation-like NAT -defined non empty V18() Function-like constant finite 1 -element FinSequence-like FinSubsequence-like set

len <*D*> is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT

len <*f*> is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT

<*D*> . 1 is set

D is finite set

f is finite set

card f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of omega

card D is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of omega

D is set

<*D*> is Relation-like NAT -defined non empty V18() Function-like constant finite 1 -element FinSequence-like FinSubsequence-like set

f is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

f ^ <*D*> is Relation-like NAT -defined non empty Function-like finite FinSequence-like FinSubsequence-like set

a is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

k is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

(f ^ <*D*>) ^ k is Relation-like NAT -defined non empty Function-like finite FinSequence-like FinSubsequence-like set

<*D*> ^ k is Relation-like NAT -defined non empty Function-like finite FinSequence-like FinSubsequence-like set

f ^ (<*D*> ^ k) is Relation-like NAT -defined non empty Function-like finite FinSequence-like FinSubsequence-like set

len f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT

len (f ^ <*D*>) is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT

len k is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT

(len (f ^ <*D*>)) + (len k) is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT

len <*D*> is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT

(len f) + (len <*D*>) is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT

((len f) + (len <*D*>)) + (len k) is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT

(len f) + 1 is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT

((len f) + 1) + (len k) is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT

D is set

<*D*> is Relation-like NAT -defined non empty V18() Function-like constant finite 1 -element FinSequence-like FinSubsequence-like set

f is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

a is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

a ^ <*D*> is Relation-like NAT -defined non empty Function-like finite FinSequence-like FinSubsequence-like set

k is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

f ^ k is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

k ^ <*D*> is Relation-like NAT -defined non empty Function-like finite FinSequence-like FinSubsequence-like set

f ^ (k ^ <*D*>) is Relation-like NAT -defined non empty Function-like finite FinSequence-like FinSubsequence-like set

len a is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT

len (a ^ <*D*>) is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT

len k is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT

(len (a ^ <*D*>)) + (len k) is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT

len <*D*> is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT

(len a) + (len <*D*>) is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT

((len a) + (len <*D*>)) + (len k) is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT

(len a) + 1 is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT

((len a) + 1) + (len k) is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT

D is set

<*D*> is Relation-like NAT -defined non empty V18() Function-like constant finite 1 -element FinSequence-like FinSubsequence-like set

f is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

a is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

a ^ <*D*> is Relation-like NAT -defined non empty Function-like finite FinSequence-like FinSubsequence-like set

len f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT

len (a ^ <*D*>) is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT

len a is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT

len <*D*> is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT

(len a) + (len <*D*>) is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT

(len a) + 1 is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT

k is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

f ^ k is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

k is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

f ^ k is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

D is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

f is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

f ^ D is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

len f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT

len D is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT

(len f) + (len D) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT

D is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

rng D is finite set

(rng D) * is non empty functional FinSequence-membered FinSequenceSet of rng D

a is set

k is set

x is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

rng x is finite set

y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT

Seg y is finite y -element Element of K40(NAT)

D | (Seg y) is Relation-like NAT -defined Seg y -defined NAT -defined Function-like finite FinSubsequence-like set

y is Relation-like NAT -defined rng D -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of rng D

f is set

a is set

k is set

x is set

y is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

k is set

x is set

y is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

D is set

f is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

(f) is set

a is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

D is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

f is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

(f) is set

a is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

D is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

f is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

(f) is set

len f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT

len D is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT

f is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

a is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

f ^ a is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

D is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

(D) is set

({}) is set

the Element of ({}) is Element of ({})

f is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

{{}} is non empty V18() functional finite V37() 1 -element set

f is set

<*f*> is Relation-like NAT -defined non empty V18() Function-like constant finite 1 -element FinSequence-like FinSubsequence-like set

(<*f*>) is set

a is set

k is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

len <*f*> is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT

len k is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT

0 + 1 is epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V16() non empty V20() finite cardinal Element of NAT

a is set

f is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

a is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

(f) is set

(a) is set

k is set

x is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

a is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

f is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

(f) is set

k is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

x is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

x is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT

Seg x is finite x -element Element of K40(NAT)

f | (Seg x) is Relation-like NAT -defined Seg x -defined NAT -defined Function-like finite FinSubsequence-like set

y is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT

Seg y is finite y -element Element of K40(NAT)

f | (Seg y) is Relation-like NAT -defined Seg y -defined NAT -defined Function-like finite FinSubsequence-like set

k | (Seg x) is Relation-like NAT -defined Seg x -defined NAT -defined Function-like finite FinSubsequence-like set

a | (Seg y) is Relation-like NAT -defined Seg y -defined NAT -defined Function-like finite FinSubsequence-like set

NAT * is non empty functional FinSequence-membered FinSequenceSet of NAT

f is set

f is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

(f) is set

f is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

a is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT

<*a*> is Relation-like NAT -defined NAT -valued non empty V18() Function-like constant finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT

f ^ <*a*> is Relation-like NAT -defined NAT -valued non empty Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

k is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT

<*k*> is Relation-like NAT -defined NAT -valued non empty V18() Function-like constant finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT

f ^ <*k*> is Relation-like NAT -defined NAT -valued non empty Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

<*> NAT is Relation-like non-empty empty-yielding NAT -defined NAT -valued epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural ext-real non positive non negative V16() empty V20() Function-like one-to-one constant functional finite finite-yielding V37() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V44() V45() FinSequence of NAT

{(<*> NAT)} is non empty V18() functional finite V37() 1 -element set

f is non empty V18() functional finite V37() 1 -element set

f is set

a is non empty () set

f is non empty () set

a is Element of f

f is non empty () set

a is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

k is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

x is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like (f)

(x) is set

(a) is set

f is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

a is non empty () set

k is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

f ^ k is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

x is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

len f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT

Seg (len f) is finite len f -element Element of K40(NAT)

x | (Seg (len f)) is Relation-like NAT -defined Seg (len f) -defined NAT -defined NAT -valued Function-like finite FinSubsequence-like set

len x is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT

len k is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT

(len f) + (len k) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT

y is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

len y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT

z is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal set

dom f is finite Element of K40(NAT)

x . z is set

f . z is set

y . z is set

(x) is set

<*> NAT is Relation-like non-empty empty-yielding NAT -defined NAT -valued epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural ext-real non positive non negative V16() empty V20() Function-like one-to-one constant functional finite finite-yielding V37() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V44() V45() FinSequence of NAT

f is non empty () set

the Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like (f) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like (f)

a is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

{} ^ a is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

f is non empty () set

a is non empty () set

f \/ a is non empty set

x is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

(x) is set

x is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT

<*y*> is Relation-like NAT -defined NAT -valued non empty V18() Function-like constant finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT

x ^ <*y*> is Relation-like NAT -defined NAT -valued non empty Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

z is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT

<*z*> is Relation-like NAT -defined NAT -valued non empty V18() Function-like constant finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT

x ^ <*z*> is Relation-like NAT -defined NAT -valued non empty Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

f /\ a is set

x is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

(x) is set

x is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT

<*y*> is Relation-like NAT -defined NAT -valued non empty V18() Function-like constant finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT

x ^ <*y*> is Relation-like NAT -defined NAT -valued non empty Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

z is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT

<*z*> is Relation-like NAT -defined NAT -valued non empty V18() Function-like constant finite 1 -element FinSequence-like FinSubsequence-like FinSequence of NAT

x ^ <*z*> is Relation-like NAT -defined NAT -valued non empty Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

f is non empty () set

a is non empty () set

f \/ a is non empty () set

f is non empty () set

a is non empty () set

f /\ a is non empty () set

f is non empty finite () set

a is non empty finite () set

f \/ a is non empty finite () set

a is non empty finite () set

f is non empty () set

a /\ f is non empty finite () set

f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V16() V20() finite cardinal Element of NAT

{ <*b

{ <*b

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

{ <*b

{ <*b

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

{ <*b

{ <*b

(0) is non empty finite () set

{ <*b

{ <*b

the Element of { <*b

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

{ <*b

{ <*b

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)

{ b

{ (a ^ b

{ b

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

{ b

k is non empty () set

(a,f,k) is non empty () set

{ (f ^ b

{ b

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

{ b

x is set

y is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like (f)

{ (a ^ b

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

{ b

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