:: ZF_LANG semantic presentation

REAL is set
NAT is non empty V8() V9() V10() V33() V38() V39() Element of K12(REAL)
K12(REAL) is non empty set
NAT is non empty V8() V9() V10() V33() V38() V39() set
K12(NAT) is non empty V33() set
K12(NAT) is non empty V33() set
{} is ext-real V4() empty V8() V9() V10() V12() V13() V14() V15() functional V33() V38() V40( {} ) FinSequence-membered set
1 is ext-real positive V4() non empty V8() V9() V10() V14() V15() V33() V38() Element of NAT
2 is ext-real positive V4() non empty V8() V9() V10() V14() V15() V33() V38() Element of NAT
3 is ext-real positive V4() non empty V8() V9() V10() V14() V15() V33() V38() Element of NAT
0 is ext-real V4() empty V8() V9() V10() V12() V13() V14() V15() functional V33() V38() V40( {} ) FinSequence-membered Element of NAT
Seg 1 is non empty V6() V33() V40(1) Element of K12(NAT)
5 is ext-real positive V4() non empty V8() V9() V10() V14() V15() V33() V38() Element of NAT
{ b₁ where b₁ is ext-real V4() V8() V9() V10() V14() V15() V33() V38() Element of NAT : 5 <= b₁ } is set
H is set
F is ext-real V4() V8() V9() V10() V14() V15() V33() V38() Element of NAT
() is Element of K12(NAT)
H is ext-real V4() V8() V9() V10() V14() V15() V33() V38() Element of NAT
5 + H is ext-real V4() V8() V9() V10() V14() V15() V33() V38() Element of NAT
H is Element of ()
<*H*> is non empty V6() Relation-like NAT -defined Function-like V33() V40(1) FinSequence-like FinSubsequence-like set
H is non empty Element of K12(NAT)
F is Element of H
F is ext-real V4() V8() V9() V10() V14() V15() V33() V38() Element of NAT
<*F*> is non empty V6() Relation-like NAT -defined NAT -valued Function-like V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*0*> is non empty V6() Relation-like NAT -defined NAT -valued Function-like V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
H is Element of ()
(H) is non empty V6() Relation-like NAT -defined NAT -valued Function-like V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*0*> ^ (H) is non empty Relation-like NAT -defined NAT -valued Function-like V33() V40(1 + 1) FinSequence-like FinSubsequence-like FinSequence of NAT
1 + 1 is ext-real V4() V8() V9() V10() V14() V15() V33() V38() Element of NAT
H is Element of ()
(H) is non empty V6() Relation-like NAT -defined NAT -valued Function-like V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
(<*0*> ^ (H)) ^ (H) is non empty Relation-like NAT -defined NAT -valued Function-like V33() V40((1 + 1) + 1) FinSequence-like FinSubsequence-like FinSequence of NAT
(1 + 1) + 1 is ext-real V4() V8() V9() V10() V14() V15() V33() V38() Element of NAT
<*1*> is non empty V6() Relation-like NAT -defined NAT -valued Function-like V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*1*> ^ (H) is non empty Relation-like NAT -defined NAT -valued Function-like V33() V40(1 + 1) FinSequence-like FinSubsequence-like FinSequence of NAT
(<*1*> ^ (H)) ^ (H) is non empty Relation-like NAT -defined NAT -valued Function-like V33() V40((1 + 1) + 1) FinSequence-like FinSubsequence-like FinSequence of NAT
H is Element of ()
H is Element of ()
(H,H) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
(H) is non empty V6() Relation-like NAT -defined NAT -valued Function-like V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*0*> ^ (H) is non empty Relation-like NAT -defined NAT -valued Function-like V33() V40(1 + 1) FinSequence-like FinSubsequence-like FinSequence of NAT
(H) is non empty V6() Relation-like NAT -defined NAT -valued Function-like V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
(<*0*> ^ (H)) ^ (H) is non empty Relation-like NAT -defined NAT -valued Function-like V33() V40((1 + 1) + 1) FinSequence-like FinSubsequence-like FinSequence of NAT
F is Element of ()
F is Element of ()
(F,F) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
(F) is non empty V6() Relation-like NAT -defined NAT -valued Function-like V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*0*> ^ (F) is non empty Relation-like NAT -defined NAT -valued Function-like V33() V40(1 + 1) FinSequence-like FinSubsequence-like FinSequence of NAT
(F) is non empty V6() Relation-like NAT -defined NAT -valued Function-like V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
(<*0*> ^ (F)) ^ (F) is non empty Relation-like NAT -defined NAT -valued Function-like V33() V40((1 + 1) + 1) FinSequence-like FinSubsequence-like FinSequence of NAT
(H) ^ (H) is non empty Relation-like NAT -defined NAT -valued Function-like V33() V40(1 + 1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*0*> ^ ((H) ^ (H)) is non empty Relation-like NAT -defined NAT -valued Function-like V33() V40(1 + (1 + 1)) FinSequence-like FinSubsequence-like FinSequence of NAT
1 + (1 + 1) is ext-real V4() V8() V9() V10() V14() V15() V33() V38() Element of NAT
(F) ^ (F) is non empty Relation-like NAT -defined NAT -valued Function-like V33() V40(1 + 1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*0*> ^ ((F) ^ (F)) is non empty Relation-like NAT -defined NAT -valued Function-like V33() V40(1 + (1 + 1)) FinSequence-like FinSubsequence-like FinSequence of NAT
<*H,H*> is non empty Relation-like NAT -defined Function-like V33() V40(2) FinSequence-like FinSubsequence-like set
<*H,H*> . 1 is set
<*H,H*> . 2 is set
<*F,F*> is non empty Relation-like NAT -defined Function-like V33() V40(2) FinSequence-like FinSubsequence-like set
<*F,F*> . 1 is set
<*F,F*> . 2 is set
H is Element of ()
H is Element of ()
(H,H) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
(H) is non empty V6() Relation-like NAT -defined NAT -valued Function-like V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*1*> ^ (H) is non empty Relation-like NAT -defined NAT -valued Function-like V33() V40(1 + 1) FinSequence-like FinSubsequence-like FinSequence of NAT
(H) is non empty V6() Relation-like NAT -defined NAT -valued Function-like V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
(<*1*> ^ (H)) ^ (H) is non empty Relation-like NAT -defined NAT -valued Function-like V33() V40((1 + 1) + 1) FinSequence-like FinSubsequence-like FinSequence of NAT
F is Element of ()
F is Element of ()
(F,F) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
(F) is non empty V6() Relation-like NAT -defined NAT -valued Function-like V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*1*> ^ (F) is non empty Relation-like NAT -defined NAT -valued Function-like V33() V40(1 + 1) FinSequence-like FinSubsequence-like FinSequence of NAT
(F) is non empty V6() Relation-like NAT -defined NAT -valued Function-like V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
(<*1*> ^ (F)) ^ (F) is non empty Relation-like NAT -defined NAT -valued Function-like V33() V40((1 + 1) + 1) FinSequence-like FinSubsequence-like FinSequence of NAT
(H) ^ (H) is non empty Relation-like NAT -defined NAT -valued Function-like V33() V40(1 + 1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*1*> ^ ((H) ^ (H)) is non empty Relation-like NAT -defined NAT -valued Function-like V33() V40(1 + (1 + 1)) FinSequence-like FinSubsequence-like FinSequence of NAT
1 + (1 + 1) is ext-real V4() V8() V9() V10() V14() V15() V33() V38() Element of NAT
(F) ^ (F) is non empty Relation-like NAT -defined NAT -valued Function-like V33() V40(1 + 1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*1*> ^ ((F) ^ (F)) is non empty Relation-like NAT -defined NAT -valued Function-like V33() V40(1 + (1 + 1)) FinSequence-like FinSubsequence-like FinSequence of NAT
<*H,H*> is non empty Relation-like NAT -defined Function-like V33() V40(2) FinSequence-like FinSubsequence-like set
<*H,H*> . 1 is set
<*H,H*> . 2 is set
<*F,F*> is non empty Relation-like NAT -defined Function-like V33() V40(2) FinSequence-like FinSubsequence-like set
<*F,F*> . 1 is set
<*F,F*> . 2 is set
<*2*> is non empty V6() Relation-like NAT -defined NAT -valued Function-like V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
H is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
<*2*> ^ H is non empty Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
<*3*> is non empty V6() Relation-like NAT -defined NAT -valued Function-like V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*3*> ^ H is non empty Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
H is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
(<*3*> ^ H) ^ H is non empty Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
4 is ext-real positive V4() non empty V8() V9() V10() V14() V15() V33() V38() Element of NAT
<*4*> is non empty V6() Relation-like NAT -defined NAT -valued Function-like V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
H is Element of ()
(H) is non empty V6() Relation-like NAT -defined NAT -valued Function-like V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*4*> ^ (H) is non empty Relation-like NAT -defined NAT -valued Function-like V33() V40(1 + 1) FinSequence-like FinSubsequence-like FinSequence of NAT
H is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
(<*4*> ^ (H)) ^ H is non empty Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
H is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
H is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
F is Element of ()
(F,H) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
(F) is non empty V6() Relation-like NAT -defined NAT -valued Function-like V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*4*> ^ (F) is non empty Relation-like NAT -defined NAT -valued Function-like V33() V40(1 + 1) FinSequence-like FinSubsequence-like FinSequence of NAT
(<*4*> ^ (F)) ^ H is non empty Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
F is Element of ()
(F,H) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
(F) is non empty V6() Relation-like NAT -defined NAT -valued Function-like V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*4*> ^ (F) is non empty Relation-like NAT -defined NAT -valued Function-like V33() V40(1 + 1) FinSequence-like FinSubsequence-like FinSequence of NAT
(<*4*> ^ (F)) ^ H is non empty Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
(F) ^ H is non empty Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
<*4*> ^ ((F) ^ H) is non empty Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
(F) ^ H is non empty Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
<*4*> ^ ((F) ^ H) is non empty Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
((F) ^ H) . 1 is set
((F) ^ H) . 1 is set
NAT * is non empty functional FinSequence-membered set
H is set
(0) is Element of ()
5 + 0 is ext-real V4() V8() V9() V10() V14() V15() V33() V38() Element of NAT
((0),(0)) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
((0)) is non empty V6() Relation-like NAT -defined NAT -valued Function-like V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*0*> ^ ((0)) is non empty Relation-like NAT -defined NAT -valued Function-like V33() V40(1 + 1) FinSequence-like FinSubsequence-like FinSequence of NAT
(<*0*> ^ ((0))) ^ ((0)) is non empty Relation-like NAT -defined NAT -valued Function-like V33() V40((1 + 1) + 1) FinSequence-like FinSubsequence-like FinSequence of NAT
F is non empty set
F is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
F is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
H is non empty set
F is set
F is Element of ()
F is Element of ()
(F,F) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
(F) is non empty V6() Relation-like NAT -defined NAT -valued Function-like V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*0*> ^ (F) is non empty Relation-like NAT -defined NAT -valued Function-like V33() V40(1 + 1) FinSequence-like FinSubsequence-like FinSequence of NAT
(F) is non empty V6() Relation-like NAT -defined NAT -valued Function-like V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
(<*0*> ^ (F)) ^ (F) is non empty Relation-like NAT -defined NAT -valued Function-like V33() V40((1 + 1) + 1) FinSequence-like FinSubsequence-like FinSequence of NAT
(F,F) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
<*1*> ^ (F) is non empty Relation-like NAT -defined NAT -valued Function-like V33() V40(1 + 1) FinSequence-like FinSubsequence-like FinSequence of NAT
(<*1*> ^ (F)) ^ (F) is non empty Relation-like NAT -defined NAT -valued Function-like V33() V40((1 + 1) + 1) FinSequence-like FinSubsequence-like FinSequence of NAT
L is non empty set
L is non empty set
F is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
(F) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
<*2*> ^ F is non empty Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
F is non empty set
F is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
F is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
(F,F) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
<*3*> ^ F is non empty Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
(<*3*> ^ F) ^ F is non empty Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
L is non empty set
F is Element of ()
F is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
(F,F) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
(F) is non empty V6() Relation-like NAT -defined NAT -valued Function-like V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*4*> ^ (F) is non empty Relation-like NAT -defined NAT -valued Function-like V33() V40(1 + 1) FinSequence-like FinSubsequence-like FinSequence of NAT
(<*4*> ^ (F)) ^ F is non empty Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
L is non empty set
F is non empty set
F is set
H is non empty set
H is non empty set
() is non empty set
the Element of () is Element of ()
H is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
H is set
H is Element of ()
H is Element of ()
(H,H) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
(H) is non empty V6() Relation-like NAT -defined NAT -valued Function-like V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*0*> ^ (H) is non empty Relation-like NAT -defined NAT -valued Function-like V33() V40(1 + 1) FinSequence-like FinSubsequence-like FinSequence of NAT
(H) is non empty V6() Relation-like NAT -defined NAT -valued Function-like V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
(<*0*> ^ (H)) ^ (H) is non empty Relation-like NAT -defined NAT -valued Function-like V33() V40((1 + 1) + 1) FinSequence-like FinSubsequence-like FinSequence of NAT
(H,H) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
<*1*> ^ (H) is non empty Relation-like NAT -defined NAT -valued Function-like V33() V40(1 + 1) FinSequence-like FinSubsequence-like FinSequence of NAT
(<*1*> ^ (H)) ^ (H) is non empty Relation-like NAT -defined NAT -valued Function-like V33() V40((1 + 1) + 1) FinSequence-like FinSubsequence-like FinSequence of NAT
H is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
(H) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
<*2*> ^ H is non empty Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
H is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
(H,H) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
<*3*> ^ H is non empty Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
(<*3*> ^ H) ^ H is non empty Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
H is Element of ()
H is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
(H,H) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
(H) is non empty V6() Relation-like NAT -defined NAT -valued Function-like V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*4*> ^ (H) is non empty Relation-like NAT -defined NAT -valued Function-like V33() V40(1 + 1) FinSequence-like FinSubsequence-like FinSequence of NAT
(<*4*> ^ (H)) ^ H is non empty Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
H is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
H is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
F is Element of ()
F is Element of ()
(F,F) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
(F) is non empty V6() Relation-like NAT -defined NAT -valued Function-like V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*0*> ^ (F) is non empty Relation-like NAT -defined NAT -valued Function-like V33() V40(1 + 1) FinSequence-like FinSubsequence-like FinSequence of NAT
(F) is non empty V6() Relation-like NAT -defined NAT -valued Function-like V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
(<*0*> ^ (F)) ^ (F) is non empty Relation-like NAT -defined NAT -valued Function-like V33() V40((1 + 1) + 1) FinSequence-like FinSubsequence-like FinSequence of NAT
L is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
k is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
k is Element of ()
L1 is Element of ()
(k,L1) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
(k) is non empty V6() Relation-like NAT -defined NAT -valued Function-like V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*1*> ^ (k) is non empty Relation-like NAT -defined NAT -valued Function-like V33() V40(1 + 1) FinSequence-like FinSubsequence-like FinSequence of NAT
(L1) is non empty V6() Relation-like NAT -defined NAT -valued Function-like V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
(<*1*> ^ (k)) ^ (L1) is non empty Relation-like NAT -defined NAT -valued Function-like V33() V40((1 + 1) + 1) FinSequence-like FinSubsequence-like FinSequence of NAT
m is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
F1 is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
G1 is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
(G1) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
<*2*> ^ G1 is non empty Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
j is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
F1 is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
G1 is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
c₁₅ is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
(G1,c₁₅) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
<*3*> ^ G1 is non empty Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
(<*3*> ^ G1) ^ c₁₅ is non empty Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
F1 is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
G1 is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
F1 is Element of ()
G1 is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
(F1,G1) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
(F1) is non empty V6() Relation-like NAT -defined NAT -valued Function-like V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*4*> ^ (F1) is non empty Relation-like NAT -defined NAT -valued Function-like V33() V40(1 + 1) FinSequence-like FinSubsequence-like FinSequence of NAT
(<*4*> ^ (F1)) ^ G1 is non empty Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
H is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
(H) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
<*2*> ^ H is non empty Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
H is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
(H) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
<*2*> ^ H is non empty Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
((H),(H)) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
<*3*> ^ (H) is non empty Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
(<*3*> ^ (H)) ^ (H) is non empty Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
(((H),(H))) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
<*2*> ^ ((H),(H)) is non empty Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
(H,(H)) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
<*3*> ^ H is non empty Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
(<*3*> ^ H) ^ (H) is non empty Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
((H,(H))) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
<*2*> ^ (H,(H)) is non empty Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
H is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
H is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
(H,H) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
(H) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
<*2*> ^ H is non empty Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
(H,(H)) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
<*3*> ^ H is non empty Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
(<*3*> ^ H) ^ (H) is non empty Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
((H,(H))) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
<*2*> ^ (H,(H)) is non empty Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
(H,H) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
(H) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
<*2*> ^ H is non empty Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
(H,(H)) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
<*3*> ^ H is non empty Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
(<*3*> ^ H) ^ (H) is non empty Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
((H,(H))) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
<*2*> ^ (H,(H)) is non empty Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
((H,H),(H,H)) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
<*3*> ^ (H,H) is non empty Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
(<*3*> ^ (H,H)) ^ (H,H) is non empty Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
H is Element of ()
H is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
(H) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
<*2*> ^ H is non empty Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
(H,(H)) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
(H) is non empty V6() Relation-like NAT -defined NAT -valued Function-like V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*4*> ^ (H) is non empty Relation-like NAT -defined NAT -valued Function-like V33() V40(1 + 1) FinSequence-like FinSubsequence-like FinSequence of NAT
(<*4*> ^ (H)) ^ (H) is non empty Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
((H,(H))) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
<*2*> ^ (H,(H)) is non empty Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
H is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
H is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
F is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
F is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
(F,F) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
(F) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
<*2*> ^ F is non empty Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
(F) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
<*2*> ^ F is non empty Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
((F),(F)) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
<*3*> ^ (F) is non empty Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
(<*3*> ^ (F)) ^ (F) is non empty Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
(((F),(F))) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
<*2*> ^ ((F),(F)) is non empty Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
L is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
k is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
k is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
L1 is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
(k,L1) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
(L1) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
<*2*> ^ L1 is non empty Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
(k,(L1)) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
<*3*> ^ k is non empty Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
(<*3*> ^ k) ^ (L1) is non empty Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
((k,(L1))) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
<*2*> ^ (k,(L1)) is non empty Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
m is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
F1 is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
G1 is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
j is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
(G1,j) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
(G1,j) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
(j) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
<*2*> ^ j is non empty Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
(G1,(j)) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
<*3*> ^ G1 is non empty Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
(<*3*> ^ G1) ^ (j) is non empty Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
((G1,(j))) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
<*2*> ^ (G1,(j)) is non empty Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
(j,G1) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
(G1) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
<*2*> ^ G1 is non empty Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
(j,(G1)) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
<*3*> ^ j is non empty Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
(<*3*> ^ j) ^ (G1) is non empty Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
((j,(G1))) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
<*2*> ^ (j,(G1)) is non empty Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
((G1,j),(j,G1)) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
<*3*> ^ (G1,j) is non empty Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
(<*3*> ^ (G1,j)) ^ (j,G1) is non empty Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
F1 is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
G1 is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
c₁₅ is Element of ()
F1 is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
(c₁₅,F1) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
(F1) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
<*2*> ^ F1 is non empty Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
(c₁₅,(F1)) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
(c₁₅) is non empty V6() Relation-like NAT -defined NAT -valued Function-like V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*4*> ^ (c₁₅) is non empty Relation-like NAT -defined NAT -valued Function-like V33() V40(1 + 1) FinSequence-like FinSubsequence-like FinSequence of NAT
(<*4*> ^ (c₁₅)) ^ (F1) is non empty Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
((c₁₅,(F1))) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
<*2*> ^ (c₁₅,(F1)) is non empty Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
H is Element of ()
H is Element of ()
F is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
(H,F) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
(H) is non empty V6() Relation-like NAT -defined NAT -valued Function-like V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*4*> ^ (H) is non empty Relation-like NAT -defined NAT -valued Function-like V33() V40(1 + 1) FinSequence-like FinSubsequence-like FinSequence of NAT
(<*4*> ^ (H)) ^ F is non empty Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
(H,(H,F)) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
(H) is non empty V6() Relation-like NAT -defined NAT -valued Function-like V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*4*> ^ (H) is non empty Relation-like NAT -defined NAT -valued Function-like V33() V40(1 + 1) FinSequence-like FinSubsequence-like FinSequence of NAT
(<*4*> ^ (H)) ^ (H,F) is non empty Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
(H,F) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
(F) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
<*2*> ^ F is non empty Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
(H,(F)) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
(<*4*> ^ (H)) ^ (F) is non empty Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
((H,(F))) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
<*2*> ^ (H,(F)) is non empty Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
(H,(H,F)) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
((H,F)) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
<*2*> ^ (H,F) is non empty Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
(H,((H,F))) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
(<*4*> ^ (H)) ^ ((H,F)) is non empty Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
((H,((H,F)))) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
<*2*> ^ (H,((H,F))) is non empty Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
H is Element of ()
H is Element of ()
F is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
(H,H,F) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
(H,F) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
(H) is non empty V6() Relation-like NAT -defined NAT -valued Function-like V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*4*> ^ (H) is non empty Relation-like NAT -defined NAT -valued Function-like V33() V40(1 + 1) FinSequence-like FinSubsequence-like FinSequence of NAT
(<*4*> ^ (H)) ^ F is non empty Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
(H,(H,F)) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
(H) is non empty V6() Relation-like NAT -defined NAT -valued Function-like V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*4*> ^ (H) is non empty Relation-like NAT -defined NAT -valued Function-like V33() V40(1 + 1) FinSequence-like FinSubsequence-like FinSequence of NAT
(<*4*> ^ (H)) ^ (H,F) is non empty Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
F is Element of ()
L is Element of ()
k is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
(F,L,k) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
(L,k) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
(k) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
<*2*> ^ k is non empty Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
(L,(k)) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
(L) is non empty V6() Relation-like NAT -defined NAT -valued Function-like V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*4*> ^ (L) is non empty Relation-like NAT -defined NAT -valued Function-like V33() V40(1 + 1) FinSequence-like FinSubsequence-like FinSequence of NAT
(<*4*> ^ (L)) ^ (k) is non empty Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
((L,(k))) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
<*2*> ^ (L,(k)) is non empty Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
(F,(L,k)) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
((L,k)) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
<*2*> ^ (L,k) is non empty Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
(F,((L,k))) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
(F) is non empty V6() Relation-like NAT -defined NAT -valued Function-like V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*4*> ^ (F) is non empty Relation-like NAT -defined NAT -valued Function-like V33() V40(1 + 1) FinSequence-like FinSubsequence-like FinSequence of NAT
(<*4*> ^ (F)) ^ ((L,k)) is non empty Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
((F,((L,k)))) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
<*2*> ^ (F,((L,k))) is non empty Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
H is Element of ()
H is Element of ()
F is Element of ()
F is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
(H,F,F) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
(F,F) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
(F) is non empty V6() Relation-like NAT -defined NAT -valued Function-like V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*4*> ^ (F) is non empty Relation-like NAT -defined NAT -valued Function-like V33() V40(1 + 1) FinSequence-like FinSubsequence-like FinSequence of NAT
(<*4*> ^ (F)) ^ F is non empty Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
(H,(F,F)) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
(H) is non empty V6() Relation-like NAT -defined NAT -valued Function-like V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*4*> ^ (H) is non empty Relation-like NAT -defined NAT -valued Function-like V33() V40(1 + 1) FinSequence-like FinSubsequence-like FinSequence of NAT
(<*4*> ^ (H)) ^ (F,F) is non empty Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
(H,(H,F,F)) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
(H) is non empty V6() Relation-like NAT -defined NAT -valued Function-like V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*4*> ^ (H) is non empty Relation-like NAT -defined NAT -valued Function-like V33() V40(1 + 1) FinSequence-like FinSubsequence-like FinSequence of NAT
(<*4*> ^ (H)) ^ (H,F,F) is non empty Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
(H,F,F) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
(F,F) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
(F) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
<*2*> ^ F is non empty Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
(F,(F)) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
(<*4*> ^ (F)) ^ (F) is non empty Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
((F,(F))) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
<*2*> ^ (F,(F)) is non empty Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
(H,(F,F)) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
((F,F)) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
<*2*> ^ (F,F) is non empty Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
(H,((F,F))) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
(<*4*> ^ (H)) ^ ((F,F)) is non empty Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
((H,((F,F)))) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
<*2*> ^ (H,((F,F))) is non empty Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
(H,(H,F,F)) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
((H,F,F)) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
<*2*> ^ (H,F,F) is non empty Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
(H,((H,F,F))) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
(<*4*> ^ (H)) ^ ((H,F,F)) is non empty Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
((H,((H,F,F)))) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
<*2*> ^ (H,((H,F,F))) is non empty Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
H is Element of ()
H is Element of ()
F is Element of ()
F is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
(H,H,F,F) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
(H,F,F) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
(F,F) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
(F) is non empty V6() Relation-like NAT -defined NAT -valued Function-like V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*4*> ^ (F) is non empty Relation-like NAT -defined NAT -valued Function-like V33() V40(1 + 1) FinSequence-like FinSubsequence-like FinSequence of NAT
(<*4*> ^ (F)) ^ F is non empty Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
(H,(F,F)) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
(H) is non empty V6() Relation-like NAT -defined NAT -valued Function-like V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*4*> ^ (H) is non empty Relation-like NAT -defined NAT -valued Function-like V33() V40(1 + 1) FinSequence-like FinSubsequence-like FinSequence of NAT
(<*4*> ^ (H)) ^ (F,F) is non empty Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
(H,(H,F,F)) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
(H) is non empty V6() Relation-like NAT -defined NAT -valued Function-like V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*4*> ^ (H) is non empty Relation-like NAT -defined NAT -valued Function-like V33() V40(1 + 1) FinSequence-like FinSubsequence-like FinSequence of NAT
(<*4*> ^ (H)) ^ (H,F,F) is non empty Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
L is Element of ()
k is Element of ()
k is Element of ()
L1 is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
(L,k,k,L1) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
(k,k,L1) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
(k,L1) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
(L1) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
<*2*> ^ L1 is non empty Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
(k,(L1)) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
(k) is non empty V6() Relation-like NAT -defined NAT -valued Function-like V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*4*> ^ (k) is non empty Relation-like NAT -defined NAT -valued Function-like V33() V40(1 + 1) FinSequence-like FinSubsequence-like FinSequence of NAT
(<*4*> ^ (k)) ^ (L1) is non empty Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
((k,(L1))) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
<*2*> ^ (k,(L1)) is non empty Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
(k,(k,L1)) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
((k,L1)) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
<*2*> ^ (k,L1) is non empty Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
(k,((k,L1))) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
(k) is non empty V6() Relation-like NAT -defined NAT -valued Function-like V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*4*> ^ (k) is non empty Relation-like NAT -defined NAT -valued Function-like V33() V40(1 + 1) FinSequence-like FinSubsequence-like FinSequence of NAT
(<*4*> ^ (k)) ^ ((k,L1)) is non empty Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
((k,((k,L1)))) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
<*2*> ^ (k,((k,L1))) is non empty Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
(L,(k,k,L1)) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
((k,k,L1)) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
<*2*> ^ (k,k,L1) is non empty Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
(L,((k,k,L1))) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
(L) is non empty V6() Relation-like NAT -defined NAT -valued Function-like V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*4*> ^ (L) is non empty Relation-like NAT -defined NAT -valued Function-like V33() V40(1 + 1) FinSequence-like FinSubsequence-like FinSequence of NAT
(<*4*> ^ (L)) ^ ((k,k,L1)) is non empty Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
((L,((k,k,L1)))) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
<*2*> ^ (L,((k,k,L1))) is non empty Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
H is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
(0) is Element of ()
5 + 0 is ext-real V4() V8() V9() V10() V14() V15() V33() V38() Element of NAT
(1) is Element of ()
5 + 1 is ext-real V4() V8() V9() V10() V14() V15() V33() V38() Element of NAT
((0),(1)) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
((0)) is non empty V6() Relation-like NAT -defined NAT -valued Function-like V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*0*> ^ ((0)) is non empty Relation-like NAT -defined NAT -valued Function-like V33() V40(1 + 1) FinSequence-like FinSubsequence-like FinSequence of NAT
((1)) is non empty V6() Relation-like NAT -defined NAT -valued Function-like V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
(<*0*> ^ ((0))) ^ ((1)) is non empty Relation-like NAT -defined NAT -valued Function-like V33() V40((1 + 1) + 1) FinSequence-like FinSubsequence-like FinSequence of NAT
{H} is non empty V6() V40(1) set
H is Element of ()
F is Element of ()
(H,F) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
(H) is non empty V6() Relation-like NAT -defined NAT -valued Function-like V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*0*> ^ (H) is non empty Relation-like NAT -defined NAT -valued Function-like V33() V40(1 + 1) FinSequence-like FinSubsequence-like FinSequence of NAT
(F) is non empty V6() Relation-like NAT -defined NAT -valued Function-like V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
(<*0*> ^ (H)) ^ (F) is non empty Relation-like NAT -defined NAT -valued Function-like V33() V40((1 + 1) + 1) FinSequence-like FinSubsequence-like FinSequence of NAT
() \ {H} is Element of K12(())
K12(()) is non empty set
(H,F) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
<*1*> ^ (H) is non empty Relation-like NAT -defined NAT -valued Function-like V33() V40(1 + 1) FinSequence-like FinSubsequence-like FinSequence of NAT
(<*1*> ^ (H)) ^ (F) is non empty Relation-like NAT -defined NAT -valued Function-like V33() V40((1 + 1) + 1) FinSequence-like FinSubsequence-like FinSequence of NAT
F is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
H is Element of ()
F is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
(H,F) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
(H) is non empty V6() Relation-like NAT -defined NAT -valued Function-like V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*4*> ^ (H) is non empty Relation-like NAT -defined NAT -valued Function-like V33() V40(1 + 1) FinSequence-like FinSubsequence-like FinSequence of NAT
(<*4*> ^ (H)) ^ F is non empty Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
(H,F) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
(<*4*> ^ (H)) ^ F is non empty Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
H is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
F is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
F is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
L is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
(F,L) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
<*3*> ^ F is non empty Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
(<*3*> ^ F) ^ L is non empty Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
(H,F) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
<*3*> ^ H is non empty Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
(<*3*> ^ H) ^ F is non empty Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
H is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
F is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
(F) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
<*2*> ^ F is non empty Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
(H) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
<*2*> ^ H is non empty Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
H is set
H is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
H is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
len H is ext-real V4() V8() V9() V10() V14() V15() V33() V38() Element of NAT
H is Element of ()
F is Element of ()
(H,F) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
(H) is non empty V6() Relation-like NAT -defined NAT -valued Function-like V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*0*> ^ (H) is non empty Relation-like NAT -defined NAT -valued Function-like V33() V40(1 + 1) FinSequence-like FinSubsequence-like FinSequence of NAT
(F) is non empty V6() Relation-like NAT -defined NAT -valued Function-like V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
(<*0*> ^ (H)) ^ (F) is non empty Relation-like NAT -defined NAT -valued Function-like V33() V40((1 + 1) + 1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*0,H,F*> is non empty Relation-like NAT -defined Function-like V33() V40(3) FinSequence-like FinSubsequence-like set
H is Element of ()
F is Element of ()
(H,F) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
(H) is non empty V6() Relation-like NAT -defined NAT -valued Function-like V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*1*> ^ (H) is non empty Relation-like NAT -defined NAT -valued Function-like V33() V40(1 + 1) FinSequence-like FinSubsequence-like FinSequence of NAT
(F) is non empty V6() Relation-like NAT -defined NAT -valued Function-like V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
(<*1*> ^ (H)) ^ (F) is non empty Relation-like NAT -defined NAT -valued Function-like V33() V40((1 + 1) + 1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*1,H,F*> is non empty Relation-like NAT -defined Function-like V33() V40(3) FinSequence-like FinSubsequence-like set
H is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
len H is ext-real V4() V8() V9() V10() V14() V15() V33() V38() Element of NAT
H is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
F is Element of ()
F is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
(F,F) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
(F) is non empty V6() Relation-like NAT -defined NAT -valued Function-like V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*4*> ^ (F) is non empty Relation-like NAT -defined NAT -valued Function-like V33() V40(1 + 1) FinSequence-like FinSubsequence-like FinSequence of NAT
(<*4*> ^ (F)) ^ F is non empty Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
<*4,F*> is non empty Relation-like NAT -defined Function-like V33() V40(2) FinSequence-like FinSubsequence-like set
len <*4,F*> is ext-real V4() non empty V8() V9() V10() V14() V15() V33() V38() Element of NAT
1 + 1 is ext-real V4() V8() V9() V10() V14() V15() V33() V38() Element of NAT
L is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
len L is ext-real V4() V8() V9() V10() V14() V15() V33() V38() Element of NAT
(1 + 1) + (len L) is ext-real V4() V8() V9() V10() V14() V15() V33() V38() Element of NAT
1 + (len L) is ext-real V4() V8() V9() V10() V14() V15() V33() V38() Element of NAT
1 + (1 + (len L)) is ext-real V4() V8() V9() V10() V14() V15() V33() V38() Element of NAT
len H is ext-real V4() V8() V9() V10() V14() V15() V33() V38() Element of NAT
len (<*4*> ^ (F)) is ext-real V4() non empty V8() V9() V10() V14() V15() V33() V38() Element of NAT
(len (<*4*> ^ (F))) + (len L) is ext-real V4() V8() V9() V10() V14() V15() V33() V38() Element of NAT
(len L) + 1 is ext-real V4() V8() V9() V10() V14() V15() V33() V38() Element of NAT
H is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
F is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
(F) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
<*2*> ^ F is non empty Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
len H is ext-real V4() V8() V9() V10() V14() V15() V33() V38() Element of NAT
len <*2*> is ext-real V4() non empty V8() V9() V10() V14() V15() V33() V38() Element of NAT
F is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
len F is ext-real V4() V8() V9() V10() V14() V15() V33() V38() Element of NAT
(len <*2*>) + (len F) is ext-real V4() V8() V9() V10() V14() V15() V33() V38() Element of NAT
(len F) + 1 is ext-real V4() V8() V9() V10() V14() V15() V33() V38() Element of NAT
H is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
F is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
F is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
(F,F) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
<*3*> ^ F is non empty Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
(<*3*> ^ F) ^ F is non empty Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
L is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
<*3*> ^ L is non empty Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
len (<*3*> ^ L) is ext-real V4() non empty V8() V9() V10() V14() V15() V33() V38() Element of NAT
len <*3*> is ext-real V4() non empty V8() V9() V10() V14() V15() V33() V38() Element of NAT
len L is ext-real V4() V8() V9() V10() V14() V15() V33() V38() Element of NAT
(len <*3*>) + (len L) is ext-real V4() V8() V9() V10() V14() V15() V33() V38() Element of NAT
len H is ext-real V4() V8() V9() V10() V14() V15() V33() V38() Element of NAT
len F is ext-real V4() V8() V9() V10() V14() V15() V33() V38() Element of NAT
(len (<*3*> ^ L)) + (len F) is ext-real V4() V8() V9() V10() V14() V15() V33() V38() Element of NAT
(len L) + 1 is ext-real V4() V8() V9() V10() V14() V15() V33() V38() Element of NAT
H is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
len H is ext-real V4() V8() V9() V10() V14() V15() V33() V38() Element of NAT
H is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
len H is ext-real V4() V8() V9() V10() V14() V15() V33() V38() Element of NAT
(len H) + 1 is ext-real V4() V8() V9() V10() V14() V15() V33() V38() Element of NAT
F is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
len F is ext-real V4() V8() V9() V10() V14() V15() V33() V38() Element of NAT
(len F) + 1 is ext-real V4() V8() V9() V10() V14() V15() V33() V38() Element of NAT
F is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
len F is ext-real V4() V8() V9() V10() V14() V15() V33() V38() Element of NAT
(len F) + 1 is ext-real V4() V8() V9() V10() V14() V15() V33() V38() Element of NAT
0 + 1 is ext-real V4() V8() V9() V10() V14() V15() V33() V38() Element of NAT
1 + 1 is ext-real V4() V8() V9() V10() V14() V15() V33() V38() Element of NAT
2 + 1 is ext-real V4() V8() V9() V10() V14() V15() V33() V38() Element of NAT
((len F) + 1) + 1 is ext-real V4() V8() V9() V10() V14() V15() V33() V38() Element of NAT
3 + 1 is ext-real V4() V8() V9() V10() V14() V15() V33() V38() Element of NAT
(3 + 1) + 1 is ext-real V4() V8() V9() V10() V14() V15() V33() V38() Element of NAT
H is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
len H is ext-real V4() V8() V9() V10() V14() V15() V33() V38() Element of NAT
H is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
len H is ext-real V4() V8() V9() V10() V14() V15() V33() V38() Element of NAT
(len H) + 1 is ext-real V4() V8() V9() V10() V14() V15() V33() V38() Element of NAT
3 + 1 is ext-real V4() V8() V9() V10() V14() V15() V33() V38() Element of NAT
H is Element of ()
H is Element of ()
(H,H) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
(H) is non empty V6() Relation-like NAT -defined NAT -valued Function-like V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*0*> ^ (H) is non empty Relation-like NAT -defined NAT -valued Function-like V33() V40(1 + 1) FinSequence-like FinSubsequence-like FinSequence of NAT
(H) is non empty V6() Relation-like NAT -defined NAT -valued Function-like V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
(<*0*> ^ (H)) ^ (H) is non empty Relation-like NAT -defined NAT -valued Function-like V33() V40((1 + 1) + 1) FinSequence-like FinSubsequence-like FinSequence of NAT
(H,H) . 1 is set
(H,H) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
<*1*> ^ (H) is non empty Relation-like NAT -defined NAT -valued Function-like V33() V40(1 + 1) FinSequence-like FinSubsequence-like FinSequence of NAT
(<*1*> ^ (H)) ^ (H) is non empty Relation-like NAT -defined NAT -valued Function-like V33() V40((1 + 1) + 1) FinSequence-like FinSubsequence-like FinSequence of NAT
(H,H) . 1 is set
(H) ^ (H) is non empty Relation-like NAT -defined NAT -valued Function-like V33() V40(1 + 1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*0*> ^ ((H) ^ (H)) is non empty Relation-like NAT -defined NAT -valued Function-like V33() V40(1 + (1 + 1)) FinSequence-like FinSubsequence-like FinSequence of NAT
1 + (1 + 1) is ext-real V4() V8() V9() V10() V14() V15() V33() V38() Element of NAT
(<*0*> ^ ((H) ^ (H))) . 1 is set
<*1*> ^ ((H) ^ (H)) is non empty Relation-like NAT -defined NAT -valued Function-like V33() V40(1 + (1 + 1)) FinSequence-like FinSubsequence-like FinSequence of NAT
(<*1*> ^ ((H) ^ (H))) . 1 is set
H is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
H is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
(H,H) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
<*3*> ^ H is non empty Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
(<*3*> ^ H) ^ H is non empty Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
(H,H) . 1 is set
H ^ H is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
<*3*> ^ (H ^ H) is non empty Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of NAT
(<*3*> ^ (H ^ H)) . 1 is set
H is Element of ()
H is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
(H,H) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like () FinSequence of NAT
(H) is non empty V6() Relation-like NAT -defined NAT -valued Function-like V33() V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
<*4*>