:: GRAPH_2 semantic presentation

REAL is non empty non trivial non finite V81() V82() V83() V87() V90() V91() V93() set
NAT is ordinal non empty non trivial non finite cardinal limit_cardinal V81() V82() V83() V84() V85() V86() V87() V88() V90() Element of bool REAL
bool REAL is non empty non trivial non finite set
omega is ordinal non empty non trivial non finite cardinal limit_cardinal V81() V82() V83() V84() V85() V86() V87() V88() V90() set
bool omega is non empty non trivial non finite set
bool NAT is non empty non trivial non finite set
COMPLEX is non empty non trivial non finite V81() V87() set
RAT is non empty non trivial non finite V81() V82() V83() V84() V87() set

1 is ordinal natural non empty ext-real positive non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V88() V89() V90() V91() V92() V94() integer Element of NAT
INT is non empty non trivial non finite V81() V82() V83() V84() V85() V87() set
2 is ordinal natural non empty ext-real positive non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V88() V89() V90() V91() V92() V94() integer Element of NAT
3 is ordinal natural non empty ext-real positive non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V88() V89() V90() V91() V92() V94() integer Element of NAT

Seg 1 is non empty trivial finite 1 -element V81() V82() V83() V84() V85() V86() V88() V89() V90() V91() V92() Element of bool NAT
{ b1 where b1 is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT : ( 1 <= b1 & b1 <= 1 ) } is set

f + 1 is ordinal natural non empty ext-real positive non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V88() V89() V90() V91() V92() V94() integer Element of NAT

j is ext-real V31() V94() integer set
i is ext-real V31() V94() integer set
j - i is ext-real V31() V94() integer set
j is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT
(f + 1) - 1 is ext-real V31() V94() integer set
m - 1 is ext-real V31() V94() integer set
j is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT
m + 1 is ordinal natural non empty ext-real positive non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V88() V89() V90() V91() V92() V94() integer Element of NAT
(m + 1) - 1 is ext-real V31() V94() integer set
j + 1 is ordinal natural non empty ext-real positive non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V88() V89() V90() V91() V92() V94() integer Element of NAT
i is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT
i + 1 is ordinal natural non empty ext-real positive non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V88() V89() V90() V91() V92() V94() integer Element of NAT

len f is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT

len m is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT
n is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT
Seg n is finite n -element V81() V82() V83() V84() V85() V86() V90() V91() V92() Element of bool NAT
{ b1 where b1 is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT : ( 1 <= b1 & b1 <= n ) } is set

i is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT
m . i is set
f . i is set
i is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT
m . i is set
f . i is set
f is set

dom (Sgm f) is finite V81() V82() V83() V84() V85() V86() V90() V91() V92() Element of bool NAT
m is set

is Relation-like RAT -valued INT -valued non empty non trivial V32() V33() V34() V35() non finite set
bool is non empty non trivial non finite set

rng ((Sgm f) | m) is finite V81() V82() V83() V84() V85() V86() V90() V91() V92() set

n is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT
Seg n is finite n -element V81() V82() V83() V84() V85() V86() V90() V91() V92() Element of bool NAT
{ b1 where b1 is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT : ( 1 <= b1 & b1 <= n ) } is set
len (Sgm f) is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT
Seg (len (Sgm f)) is finite len (Sgm f) -element V81() V82() V83() V84() V85() V86() V90() V91() V92() Element of bool NAT
{ b1 where b1 is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT : ( 1 <= b1 & b1 <= len (Sgm f) ) } is set
rng (Sgm m) is finite V81() V82() V83() V84() V85() V86() V90() V91() V92() set
i is finite set

dom (Sgm i) is finite V81() V82() V83() V84() V85() V86() V90() V91() V92() Element of bool NAT
card i is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of omega
Seg (card i) is finite card i -element V81() V82() V83() V84() V85() V86() V90() V91() V92() Element of bool NAT
{ b1 where b1 is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT : ( 1 <= b1 & b1 <= card i ) } is set
dom ((Sgm f) * (Sgm m)) is finite V81() V82() V83() V84() V85() V86() V90() V91() V92() Element of bool NAT
rng (Sgm f) is finite V81() V82() V83() V84() V85() V86() V90() V91() V92() set

rng j is finite set
rX is set

rng X is finite V81() V82() V83() V84() V85() V86() V90() V91() V92() set
dom X is finite V81() V82() V83() V84() V85() V86() V90() V91() V92() Element of bool NAT
qm is set
X . qm is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT
dom (Sgm m) is finite V81() V82() V83() V84() V85() V86() V90() V91() V92() Element of bool NAT
(Sgm m) . qm is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT
(Sgm f) . ((Sgm m) . qm) is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT
dom ((Sgm f) | m) is finite Element of bool m
bool m is set
qm is set
((Sgm f) | m) . qm is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT
(dom (Sgm f)) /\ m is finite V81() V82() V83() V84() V85() V86() V90() V91() V92() Element of bool NAT
q1 is set
(Sgm m) . q1 is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT
(Sgm f) . qm is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT
X . q1 is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT

len X is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT

X . rX is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT

X . qm is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT
(Sgm m) . rX is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT
(Sgm f) . ((Sgm m) . rX) is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT
(Sgm m) . qm is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT
(Sgm f) . ((Sgm m) . qm) is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT
len (Sgm m) is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT
mXC is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT
(Sgm m) . mXC is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT
mXC1 is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT
(Sgm m) . mXC1 is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT
mXCm is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT
fvs is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT
f is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT
{ b1 where b1 is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT : ( f <= b1 & b1 <= f + a1 ) } is set
m is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT
f + m is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT
{ b1 where b1 is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT : ( f <= b1 & b1 <= f + m ) } is set
m + 1 is ordinal natural non empty ext-real positive non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V88() V89() V90() V91() V92() V94() integer Element of NAT
f + (m + 1) is ordinal natural non empty ext-real positive non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V88() V89() V90() V91() V92() V94() integer Element of NAT
{ b1 where b1 is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT : ( f <= b1 & b1 <= f + (m + 1) ) } is set
(m + 1) + 1 is ordinal natural non empty ext-real positive non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V88() V89() V90() V91() V92() V94() integer Element of NAT
{ b1 where b1 is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT : b1 <= f + m } is set
n is finite set
j is set
j is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT
j is finite set
card j is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of omega
(f + m) + 1 is ordinal natural non empty ext-real positive non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V88() V89() V90() V91() V92() V94() integer Element of NAT
(f + m) + 0 is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT
j is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT
j is set
X is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT
(f + m) + 1 is ordinal natural non empty ext-real positive non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V88() V89() V90() V91() V92() V94() integer Element of NAT
j is finite set
{(f + (m + 1))} is non empty trivial finite V46() 1 -element V81() V82() V83() V84() V85() V86() V88() V89() V90() V91() V92() set
j \/ {(f + (m + 1))} is non empty finite set
X is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT
X is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT
{ b1 where b1 is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT : ( f <= b1 & b1 <= f + m ) } \/ {(f + (m + 1))} is non empty set
card j is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of omega
f + 0 is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT
{ b1 where b1 is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT : ( f <= b1 & b1 <= f + 0 ) } is set
0 + 1 is ordinal natural non empty ext-real positive non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V88() V89() V90() V91() V92() V94() integer Element of NAT
m is finite set
card m is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of omega
n is set
i is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT
{f} is non empty trivial finite V46() 1 -element V81() V82() V83() V84() V85() V86() V88() V89() V90() V91() V92() set
n is finite set
m is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT
f + m is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT
{ b1 where b1 is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT : ( f <= b1 & b1 <= f + m ) } is set
card n is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of omega
m + 1 is ordinal natural non empty ext-real positive non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V88() V89() V90() V91() V92() V94() integer Element of NAT
f is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT
m is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT
f + m is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT
{ b1 where b1 is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT : ( f <= b1 & b1 <= f + m ) } is set
card { b1 where b1 is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT : ( f <= b1 & b1 <= f + m ) } is ordinal cardinal set
m + 1 is ordinal natural non empty ext-real positive non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V88() V89() V90() V91() V92() V94() integer Element of NAT
{ H1(b1) where b1 is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT : ( f <= b1 & b1 <= f + m & S1[b1] ) } is set
i is finite set
{ H1(b1) where b1 is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT : ( f <= b1 & b1 <= f + m ) } is set
j is set
j is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT
j is set
j is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT
j is finite set
card j is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of omega
f is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT
m is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT
m + 1 is ordinal natural non empty ext-real positive non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V88() V89() V90() V91() V92() V94() integer Element of NAT
m + f is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT
{ b1 where b1 is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT : ( m + 1 <= b1 & b1 <= m + f ) } is set
Sgm { b1 where b1 is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT : ( m + 1 <= b1 & b1 <= m + f ) } is Relation-like NAT -defined NAT -valued Function-like V32() V33() V34() V35() finite FinSequence-like FinSubsequence-like FinSequence of NAT
Seg (m + f) is finite m + f -element V81() V82() V83() V84() V85() V86() V90() V91() V92() Element of bool NAT
{ b1 where b1 is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT : ( 1 <= b1 & b1 <= m + f ) } is set
j is set
j is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT
j is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT
(Sgm { b1 where b1 is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT : ( m + 1 <= b1 & b1 <= m + f ) } ) . j is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT
m + j is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT

(Sgm { b1 where b1 is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT : ( m + 1 <= b1 & b1 <= m + f ) } ) . j is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT
m + j is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT
j is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT
m + j is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT
(Sgm { b1 where b1 is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT : ( m + 1 <= b1 & b1 <= m + f ) } ) . j is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT
j is finite set
card j is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of omega
rX is set
m + 0 is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT
qm is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT
0 + 1 is ordinal natural non empty ext-real positive non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V88() V89() V90() V91() V92() V94() integer Element of NAT
1 - 1 is ext-real V31() V94() integer set
f - 1 is ext-real V31() V94() integer set
f -' 1 is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT
rX is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT
(m + 1) + rX is ordinal natural non empty ext-real positive non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V88() V89() V90() V91() V92() V94() integer Element of NAT
rX + 1 is ordinal natural non empty ext-real positive non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V88() V89() V90() V91() V92() V94() integer Element of NAT

len (Sgm j) is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT
rng (Sgm { b1 where b1 is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT : ( m + 1 <= b1 & b1 <= m + f ) } ) is finite V81() V82() V83() V84() V85() V86() V90() V91() V92() set
rX is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT
(Sgm { b1 where b1 is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT : ( m + 1 <= b1 & b1 <= m + f ) } ) . rX is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT
m + rX is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT
rX + 1 is ordinal natural non empty ext-real positive non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V88() V89() V90() V91() V92() V94() integer Element of NAT
(Sgm { b1 where b1 is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT : ( m + 1 <= b1 & b1 <= m + f ) } ) . (rX + 1) is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT
m + (rX + 1) is ordinal natural non empty ext-real positive non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V88() V89() V90() V91() V92() V94() integer Element of NAT
qm is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT
q1 is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT
(m + rX) + 1 is ordinal natural non empty ext-real positive non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V88() V89() V90() V91() V92() V94() integer Element of NAT
dom (Sgm { b1 where b1 is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT : ( m + 1 <= b1 & b1 <= m + f ) } ) is finite V81() V82() V83() V84() V85() V86() V90() V91() V92() Element of bool NAT
(Sgm { b1 where b1 is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT : ( m + 1 <= b1 & b1 <= m + f ) } ) . 1 is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT
q1 is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT
(Sgm { b1 where b1 is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT : ( m + 1 <= b1 & b1 <= m + f ) } ) . 0 is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT
m + 0 is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT
rX is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT
X is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT
rng (Sgm j) is finite V81() V82() V83() V84() V85() V86() V90() V91() V92() set
dom (Sgm j) is finite V81() V82() V83() V84() V85() V86() V90() V91() V92() Element of bool NAT
rX is set
(Sgm j) . rX is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT
Seg f is finite f -element V81() V82() V83() V84() V85() V86() V90() V91() V92() Element of bool NAT
{ b1 where b1 is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT : ( 1 <= b1 & b1 <= f ) } is set
qm is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT
(Sgm { b1 where b1 is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT : ( m + 1 <= b1 & b1 <= m + f ) } ) . qm is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT
m + qm is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT

len f is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT
n + 1 is ordinal natural non empty ext-real positive non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V88() V89() V90() V91() V92() V94() integer Element of NAT
(n + 1) -' m is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT

len i is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT
dom i is finite V81() V82() V83() V84() V85() V86() V90() V91() V92() Element of bool NAT
m - m is ext-real V31() V94() integer set
(n + 1) - m is ext-real V31() V94() integer set

len j is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT
(len j) + m is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT
((n + 1) - m) + m is ext-real V31() V94() integer set

j + 1 is ordinal natural non empty ext-real positive non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V88() V89() V90() V91() V92() V94() integer Element of NAT
0 + 1 is ordinal natural non empty ext-real positive non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V88() V89() V90() V91() V92() V94() integer Element of NAT
dom j is finite V81() V82() V83() V84() V85() V86() V90() V91() V92() Element of bool NAT
j . (j + 1) is set
(j + 1) - 1 is ext-real V31() V94() integer set
m + ((j + 1) - 1) is ext-real V31() V94() integer set
f . (m + ((j + 1) - 1)) is set

f . (m + j) is set

len i is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT
(len i) + m is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT

len j is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT
(len j) + m is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT

dom i is finite V81() V82() V83() V84() V85() V86() V90() V91() V92() Element of bool NAT
Seg (len i) is finite len i -element V81() V82() V83() V84() V85() V86() V90() V91() V92() Element of bool NAT
{ b1 where b1 is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT : ( 1 <= b1 & b1 <= len i ) } is set
0 + 1 is ordinal natural non empty ext-real positive non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V88() V89() V90() V91() V92() V94() integer Element of NAT
j is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT
j + 1 is ordinal natural non empty ext-real positive non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V88() V89() V90() V91() V92() V94() integer Element of NAT
i . j is set
m + j is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT
f . (m + j) is set
j . j is set

len f is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT
m is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT
n is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT
n + 1 is ordinal natural non empty ext-real positive non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V88() V89() V90() V91() V92() V94() integer Element of NAT

len (f,m,n) is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT
(len (f,m,n)) + m is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT
i is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT
i + 1 is ordinal natural non empty ext-real positive non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V88() V89() V90() V91() V92() V94() integer Element of NAT
(f,m,n) . (i + 1) is set
m + i is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT
f . (m + i) is set
i is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT
i + 1 is ordinal natural non empty ext-real positive non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V88() V89() V90() V91() V92() V94() integer Element of NAT
(f,m,n) . (i + 1) is set
m + i is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT
f . (m + i) is set

len f is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT
m is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT

f . m is set

[1,(f . m)] is non empty set
{1,(f . m)} is non empty finite set
{1} is non empty trivial finite V46() 1 -element V81() V82() V83() V84() V85() V86() V88() V89() V90() V91() V92() set
{{1,(f . m)},{1}} is non empty finite V46() set

len (f,m,m) is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT
(len (f,m,m)) + m is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT
m + 1 is ordinal natural non empty ext-real positive non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V88() V89() V90() V91() V92() V94() integer Element of NAT
0 + 1 is ordinal natural non empty ext-real positive non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V88() V89() V90() V91() V92() V94() integer Element of NAT
(f,m,m) . (0 + 1) is set
m + 0 is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT
f . (m + 0) is set

len f is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT

(len f) + 1 is ordinal natural non empty ext-real positive non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V88() V89() V90() V91() V92() V94() integer Element of NAT
len (f,1,(len f)) is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT
(len (f,1,(len f))) + 1 is ordinal natural non empty ext-real positive non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V88() V89() V90() V91() V92() V94() integer Element of NAT

dom (f,1,(len f)) is finite V81() V82() V83() V84() V85() V86() V90() V91() V92() Element of bool NAT
Seg (len f) is finite len f -element V81() V82() V83() V84() V85() V86() V90() V91() V92() Element of bool NAT
{ b1 where b1 is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT : ( 1 <= b1 & b1 <= len f ) } is set
0 + 1 is ordinal natural non empty ext-real positive non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V88() V89() V90() V91() V92() V94() integer Element of NAT
(f,1,(len f)) . n is set
f . n is set
i is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT
i + 1 is ordinal natural non empty ext-real positive non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V88() V89() V90() V91() V92() V94() integer Element of NAT

len f is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT
m is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT
m + 1 is ordinal natural non empty ext-real positive non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V88() V89() V90() V91() V92() V94() integer Element of NAT
n is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT

n + 1 is ordinal natural non empty ext-real positive non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V88() V89() V90() V91() V92() V94() integer Element of NAT
i is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT

(f,(m + 1),n) ^ (f,(n + 1),i) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

len ((f,(m + 1),n) ^ (f,(n + 1),i)) is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT
dom ((f,(m + 1),n) ^ (f,(n + 1),i)) is finite V81() V82() V83() V84() V85() V86() V90() V91() V92() Element of bool NAT
Seg (len ((f,(m + 1),n) ^ (f,(n + 1),i))) is finite len ((f,(m + 1),n) ^ (f,(n + 1),i)) -element V81() V82() V83() V84() V85() V86() V90() V91() V92() Element of bool NAT
{ b1 where b1 is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT : ( 1 <= b1 & b1 <= len ((f,(m + 1),n) ^ (f,(n + 1),i)) ) } is set
rX is ext-real V31() V94() integer set
qm is ext-real V31() V94() integer set
rX - qm is ext-real V31() V94() integer set
i + 1 is ordinal natural non empty ext-real positive non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V88() V89() V90() V91() V92() V94() integer Element of NAT
len (f,(m + 1),i) is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT
(len (f,(m + 1),i)) + (m + 1) is ordinal natural non empty ext-real positive non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V88() V89() V90() V91() V92() V94() integer Element of NAT
len (f,(m + 1),n) is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT
(len (f,(m + 1),n)) + (m + 1) is ordinal natural non empty ext-real positive non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V88() V89() V90() V91() V92() V94() integer Element of NAT
len (f,(n + 1),i) is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT
(len (f,(n + 1),i)) + (n + 1) is ordinal natural non empty ext-real positive non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V88() V89() V90() V91() V92() V94() integer Element of NAT
n - m is ext-real V31() V94() integer set
- n is ext-real non positive V31() V94() integer set
i + (- n) is ext-real V31() V94() integer set
(n - m) + (i + (- n)) is ext-real V31() V94() integer set
i - m is ext-real V31() V94() integer set

q1 is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT
0 + 1 is ordinal natural non empty ext-real positive non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V88() V89() V90() V91() V92() V94() integer Element of NAT
mXC is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT
mXC + 1 is ordinal natural non empty ext-real positive non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V88() V89() V90() V91() V92() V94() integer Element of NAT
dom (f,(m + 1),n) is finite V81() V82() V83() V84() V85() V86() V90() V91() V92() Element of bool NAT
((f,(m + 1),n) ^ (f,(n + 1),i)) . mX is set
(f,(m + 1),n) . mX is set
(m + 1) + mXC is ordinal natural non empty ext-real positive non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V88() V89() V90() V91() V92() V94() integer Element of NAT
f . ((m + 1) + mXC) is set
(f,(m + 1),i) . mX is set
q1 is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT
q1 + 1 is ordinal natural non empty ext-real positive non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V88() V89() V90() V91() V92() V94() integer Element of NAT
mXC is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT
mXC + 1 is ordinal natural non empty ext-real positive non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V88() V89() V90() V91() V92() V94() integer Element of NAT
mXC1 is ext-real V31() V94() integer set
mXC1 - q1 is ext-real V31() V94() integer set
mXCm is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT
mXCm + 1 is ordinal natural non empty ext-real positive non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V88() V89() V90() V91() V92() V94() integer Element of NAT
(len (f,(n + 1),i)) + (len (f,(m + 1),n)) is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT
(len ((f,(m + 1),n) ^ (f,(n + 1),i))) - (len (f,(m + 1),n)) is ext-real V31() V94() integer set
dom (f,(n + 1),i) is finite V81() V82() V83() V84() V85() V86() V90() V91() V92() Element of bool NAT
(n + 1) + mXCm is ordinal natural non empty ext-real positive non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V88() V89() V90() V91() V92() V94() integer Element of NAT
(m + 1) + mXC is ordinal natural non empty ext-real positive non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V88() V89() V90() V91() V92() V94() integer Element of NAT
q1 + (mXCm + 1) is ordinal natural non empty ext-real positive non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V88() V89() V90() V91() V92() V94() integer Element of NAT
((f,(m + 1),n) ^ (f,(n + 1),i)) . mX is set
(f,(n + 1),i) . (mXCm + 1) is set
f . ((n + 1) + mXCm) is set
(f,(m + 1),i) . mX is set
q1 is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT
q1 + 1 is ordinal natural non empty ext-real positive non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V88() V89() V90() V91() V92() V94() integer Element of NAT

len f is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT
m is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT

m + 1 is ordinal natural non empty ext-real positive non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V88() V89() V90() V91() V92() V94() integer Element of NAT

(f,1,m) ^ (f,(m + 1),(len f)) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
0 + 1 is ordinal natural non empty ext-real positive non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V88() V89() V90() V91() V92() V94() integer Element of NAT

len f is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT
m is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT

m + 1 is ordinal natural non empty ext-real positive non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V88() V89() V90() V91() V92() V94() integer Element of NAT
n is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT

(f,1,m) ^ (f,(m + 1),n) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
n + 1 is ordinal natural non empty ext-real positive non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V88() V89() V90() V91() V92() V94() integer Element of NAT

((f,1,m) ^ (f,(m + 1),n)) ^ (f,(n + 1),(len f)) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
0 + 1 is ordinal natural non empty ext-real positive non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V88() V89() V90() V91() V92() V94() integer Element of NAT

(f,1,n) ^ (f,(n + 1),(len f)) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

rng f is finite set
m is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT
n is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT

rng (f,m,n) is finite set
len f is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT
n + 1 is ordinal natural non empty ext-real positive non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V88() V89() V90() V91() V92() V94() integer Element of NAT
j is set
dom (f,m,n) is finite V81() V82() V83() V84() V85() V86() V90() V91() V92() Element of bool NAT
j is set
(f,m,n) . j is set
j is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT
len (f,m,n) is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT
0 + 1 is ordinal natural non empty ext-real positive non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V88() V89() V90() V91() V92() V94() integer Element of NAT
X is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT
X + 1 is ordinal natural non empty ext-real positive non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V88() V89() V90() V91() V92() V94() integer Element of NAT
(len (f,m,n)) + m is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT
m + X is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT
dom f is finite V81() V82() V83() V84() V85() V86() V90() V91() V92() Element of bool NAT
(f,m,n) . j is set
f . (m + X) is set
f is set

rng m is finite set
rng (m,n,i) is finite set

len f is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT
m is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT
f . m is set
n is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT

(f,m,n) . 1 is set
len (f,m,n) is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT
(f,m,n) . (len (f,m,n)) is set
f . n is set
n + 1 is ordinal natural non empty ext-real positive non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V88() V89() V90() V91() V92() V94() integer Element of NAT
(len (f,m,n)) + m is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT
n + 0 is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT
0 + 1 is ordinal natural non empty ext-real positive non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V88() V89() V90() V91() V92() V94() integer Element of NAT
j is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT
j + 1 is ordinal natural non empty ext-real positive non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V88() V89() V90() V91() V92() V94() integer Element of NAT
m + 0 is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT
f . (m + 0) is set
m + j is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT

len m is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT

len f is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT

len (m,f) is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT
(len (m,f)) + 1 is ordinal natural non empty ext-real positive non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V88() V89() V90() V91() V92() V94() integer Element of NAT
len m is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT
(len m) + (len f) is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT
0 + 1 is ordinal natural non empty ext-real positive non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V88() V89() V90() V91() V92() V94() integer Element of NAT
1 + 1 is ordinal natural non empty ext-real positive non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V88() V89() V90() V91() V92() V94() integer Element of NAT
(len f) + 1 is ordinal natural non empty ext-real positive non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V88() V89() V90() V91() V92() V94() integer Element of NAT
len (f,2,(len f)) is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT
(len (f,2,(len f))) + (1 + 1) is ordinal natural non empty ext-real positive non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V88() V89() V90() V91() V92() V94() integer Element of NAT
(len m) + (len (f,2,(len f))) is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86()