:: 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
{} is Relation-like non-empty empty-yielding NAT -defined RAT -valued ordinal natural Function-like one-to-one constant functional empty trivial ext-real non positive non negative V31() V32() V33() V34() V35() V36() V37() V38() V39() finite finite-yielding V46() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V81() V82() V83() V84() V85() V86() V87() V90() V91() V92() V93() V94() integer set
the Relation-like non-empty empty-yielding NAT -defined RAT -valued ordinal natural Function-like one-to-one constant functional empty trivial ext-real non positive non negative V31() V32() V33() V34() V35() V36() V37() V38() V39() finite finite-yielding V46() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V81() V82() V83() V84() V85() V86() V87() V90() V91() V92() V93() V94() integer set is Relation-like non-empty empty-yielding NAT -defined RAT -valued ordinal natural Function-like one-to-one constant functional empty trivial ext-real non positive non negative V31() V32() V33() V34() V35() V36() V37() V38() V39() finite finite-yielding V46() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V81() V82() V83() V84() V85() V86() V87() V90() V91() V92() V93() V94() integer 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
0 is Relation-like non-empty empty-yielding NAT -defined RAT -valued ordinal natural Function-like one-to-one constant functional empty trivial ext-real non positive non negative V31() V32() V33() V34() V35() V36() V37() V38() V39() finite finite-yielding V46() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V81() V82() V83() V84() V85() V86() V87() V90() V91() V92() V93() 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
{ b₁ where b₁ 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 <= b₁ & b₁ <= 1 ) } is set
card {} is Relation-like non-empty empty-yielding NAT -defined RAT -valued ordinal natural Function-like one-to-one constant functional empty trivial ext-real non positive non negative V31() V32() V33() V34() V35() V36() V37() V38() V39() finite finite-yielding V46() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V81() V82() V83() V84() V85() V86() V87() V90() V91() V92() V93() V94() integer set
f is ordinal natural ext-real non negative V31() finite cardinal V94() integer 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
m is ordinal natural ext-real non negative V31() finite cardinal V94() integer set
n is ordinal natural ext-real non negative V31() finite cardinal V94() integer set
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
f is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like 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 Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
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
{ b₁ where b₁ 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 <= b₁ & b₁ <= n ) } is set
m | (Seg n) is Relation-like NAT -defined Seg n -defined NAT -defined Function-like finite FinSequence-like FinSubsequence-like 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
Sgm f is Relation-like NAT -defined NAT -valued Function-like V32() V33() V34() V35() finite FinSequence-like FinSubsequence-like FinSequence of NAT
dom (Sgm f) is finite V81() V82() V83() V84() V85() V86() V90() V91() V92() Element of bool NAT
m is set
Sgm m is Relation-like NAT -defined NAT -valued Function-like V32() V33() V34() V35() finite FinSequence-like FinSubsequence-like FinSequence of NAT
(Sgm f) * (Sgm m) is Relation-like NAT -defined NAT -valued RAT -valued Function-like V32() V33() V34() V35() finite Element of bool [:NAT,NAT:]
[:NAT,NAT:] is Relation-like RAT -valued INT -valued non empty non trivial V32() V33() V34() V35() non finite set
bool [:NAT,NAT:] is non empty non trivial non finite set
(Sgm f) | m is Relation-like NAT -defined m -defined NAT -defined NAT -valued RAT -valued Function-like V32() V33() V34() V35() finite FinSubsequence-like Element of bool [:NAT,NAT:]
rng ((Sgm f) | m) is finite V81() V82() V83() V84() V85() V86() V90() V91() V92() set
Sgm (rng ((Sgm f) | m)) is Relation-like NAT -defined NAT -valued Function-like V32() V33() V34() V35() finite FinSequence-like FinSubsequence-like FinSequence 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
{ b₁ where b₁ 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 <= b₁ & b₁ <= 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
{ b₁ where b₁ 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 <= b₁ & b₁ <= len (Sgm f) ) } is set
rng (Sgm m) is finite V81() V82() V83() V84() V85() V86() V90() V91() V92() set
i is finite set
Sgm i is Relation-like NAT -defined NAT -valued Function-like V32() V33() V34() V35() finite FinSequence-like FinSubsequence-like FinSequence of NAT
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
{ b₁ where b₁ 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 <= b₁ & b₁ <= 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
j is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
rng j is finite set
rX is set
X is Relation-like NAT -defined NAT -valued Function-like V32() V33() V34() V35() finite FinSequence-like FinSubsequence-like FinSequence of NAT
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
rX is ordinal natural ext-real non negative V31() finite cardinal V94() integer set
qm is ordinal natural ext-real non negative V31() finite cardinal V94() integer set
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
q1 is ordinal natural ext-real non negative V31() finite cardinal V94() integer set
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
mX is ordinal natural ext-real non negative V31() finite cardinal V94() integer 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
(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
{ b₁ where b₁ 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 <= b₁ & b₁ <= f + a₁ ) } 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
{ b₁ where b₁ 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 <= b₁ & b₁ <= 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
{ b₁ where b₁ 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 <= b₁ & b₁ <= 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
{ b₁ where b₁ is ordinal natural ext-real non negative V31() finite cardinal V81() V82() V83() V84() V85() V86() V90() V91() V92() V94() integer Element of NAT : b₁ <= 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
{ b₁ where b₁ 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 <= b₁ & b₁ <= 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
{ b₁ where b₁ 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 <= b₁ & b₁ <= 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
{ b₁ where b₁ 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 <= b₁ & b₁ <= 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
{ b₁ where b₁ 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 <= b₁ & b₁ <= f + m ) } is set
card { b₁ where b₁ 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 <= b₁ & b₁ <= 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
{ H₁(b₁) where b₁ 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 <= b₁ & b₁ <= f + m & S₁[b₁] ) } is set
i is finite set
{ H₁(b₁) where b₁ 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 <= b₁ & b₁ <= 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
{ b₁ where b₁ 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 <= b₁ & b₁ <= m + f ) } is set
Sgm { b₁ where b₁ 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 <= b₁ & b₁ <= 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
{ b₁ where b₁ 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 <= b₁ & b₁ <= 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 { b₁ where b₁ 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 <= b₁ & b₁ <= 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 V94() integer set
(Sgm { b₁ where b₁ 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 <= b₁ & b₁ <= 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 { b₁ where b₁ 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 <= b₁ & b₁ <= 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
Sgm j is Relation-like NAT -defined NAT -valued Function-like V32() V33() V34() V35() finite FinSequence-like FinSubsequence-like FinSequence 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 { b₁ where b₁ 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 <= b₁ & b₁ <= 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 { b₁ where b₁ 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 <= b₁ & b₁ <= 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 { b₁ where b₁ 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 <= b₁ & b₁ <= 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 { b₁ where b₁ 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 <= b₁ & b₁ <= m + f ) } ) is finite V81() V82() V83() V84() V85() V86() V90() V91() V92() Element of bool NAT
(Sgm { b₁ where b₁ 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 <= b₁ & b₁ <= 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 { b₁ where b₁ 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 <= b₁ & b₁ <= 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
{ b₁ where b₁ 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 <= b₁ & b₁ <= 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 { b₁ where b₁ 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 <= b₁ & b₁ <= 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
m is ordinal natural ext-real non negative V31() finite cardinal V94() integer set
n is ordinal natural ext-real non negative V31() finite cardinal V94() integer set
f is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like 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
(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
i is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like 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
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
j is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like 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 is ordinal natural ext-real non negative V31() finite cardinal 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
m + j is ordinal natural ext-real non negative V31() finite cardinal V94() integer set
f . (m + j) is set
i is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like 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
j is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like 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
j is ordinal natural ext-real non negative V31() finite cardinal V94() integer set
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
{ b₁ where b₁ 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 <= b₁ & b₁ <= 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
f is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like 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
(f,m,n) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like 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
(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
f is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like 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,m) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
f . m is set
<*(f . m)*> is Relation-like NAT -defined Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like 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
{[1,(f . m)]} is Relation-like Function-like constant non empty trivial finite 1 -element 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
f is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like 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
(f,1,(len f)) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
(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
n is ordinal natural ext-real non negative V31() finite cardinal V94() integer set
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
{ b₁ where b₁ 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 <= b₁ & b₁ <= 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
f is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like 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
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,(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
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,(n + 1),i) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
(f,(m + 1),n) ^ (f,(n + 1),i) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
(f,(m + 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
{ b₁ where b₁ 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 <= b₁ & b₁ <= 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
mX is ordinal natural ext-real non negative V31() finite cardinal 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
f is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like 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,1,m) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like 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),(len f)) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
(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
(f,1,(len f)) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
f is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len 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,1,m) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like 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
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 + 1),n) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
(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,(n + 1),(len f)) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
((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) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
(f,1,n) ^ (f,(n + 1),(len f)) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
(f,1,(len f)) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
f is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
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
(f,m,n) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
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
m is Relation-like NAT -defined f -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of f
n is ordinal natural ext-real non negative V31() finite cardinal V94() integer set
i is ordinal natural ext-real non negative V31() finite cardinal V94() integer set
(m,n,i) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
rng m is finite set
rng (m,n,i) is finite set
f is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like 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) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
(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
f is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
m is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
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
(m,2,(len m)) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
f ^ (m,2,(len m)) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
f is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len 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 Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
(m,f) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
(f,2,(len f)) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
m ^ (f,2,(len f)) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
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()