:: RFINSEQ semantic presentation

REAL is non empty V12() non finite V61() V62() V63() V67() set
NAT is V12() V17() non finite cardinal limit_cardinal V61() V62() V63() V64() V65() V66() V67() Element of K19(REAL)
K19(REAL) is V12() non finite set
COMPLEX is non empty V12() non finite V61() V67() set
RAT is non empty V12() non finite V61() V62() V63() V64() V67() set
INT is non empty V12() non finite V61() V62() V63() V64() V65() V67() set
K20(COMPLEX,COMPLEX) is Relation-like V12() non finite V51() set
K19(K20(COMPLEX,COMPLEX)) is V12() non finite set
K20(K20(COMPLEX,COMPLEX),COMPLEX) is Relation-like V12() non finite V51() set
K19(K20(K20(COMPLEX,COMPLEX),COMPLEX)) is V12() non finite set
K20(REAL,REAL) is Relation-like V12() non finite V51() V52() V53() set
K19(K20(REAL,REAL)) is V12() non finite set
K20(K20(REAL,REAL),REAL) is Relation-like V12() non finite V51() V52() V53() set
K19(K20(K20(REAL,REAL),REAL)) is V12() non finite set
K20(RAT,RAT) is Relation-like RAT -valued V12() non finite V51() V52() V53() set
K19(K20(RAT,RAT)) is V12() non finite set
K20(K20(RAT,RAT),RAT) is Relation-like RAT -valued V12() non finite V51() V52() V53() set
K19(K20(K20(RAT,RAT),RAT)) is V12() non finite set
K20(INT,INT) is Relation-like RAT -valued INT -valued V12() non finite V51() V52() V53() set
K19(K20(INT,INT)) is V12() non finite set
K20(K20(INT,INT),INT) is Relation-like RAT -valued INT -valued V12() non finite V51() V52() V53() set
K19(K20(K20(INT,INT),INT)) is V12() non finite set
K20(NAT,NAT) is Relation-like RAT -valued INT -valued V51() V52() V53() V54() set
K20(K20(NAT,NAT),NAT) is Relation-like RAT -valued INT -valued V51() V52() V53() V54() set
K19(K20(K20(NAT,NAT),NAT)) is set
NAT is V12() V17() non finite cardinal limit_cardinal V61() V62() V63() V64() V65() V66() V67() set
K19(NAT) is V12() non finite set
K19(NAT) is V12() non finite set
K239(NAT) is V50() set
{} is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty V17() V21() V22() V23() ext-real non negative V33() finite finite-yielding V40() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V51() V52() V53() V54() V61() V62() V63() V64() V65() V66() V67() Function-yielding V73() set
the Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty V17() V21() V22() V23() ext-real non negative V33() finite finite-yielding V40() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V51() V52() V53() V54() V61() V62() V63() V64() V65() V66() V67() Function-yielding V73() set is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty V17() V21() V22() V23() ext-real non negative V33() finite finite-yielding V40() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V51() V52() V53() V54() V61() V62() V63() V64() V65() V66() V67() Function-yielding V73() set
1 is non empty V17() V21() V22() V23() ext-real positive non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
2 is non empty V17() V21() V22() V23() ext-real positive non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
3 is non empty V17() V21() V22() V23() ext-real positive non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
Seg 1 is non empty V12() finite 1 -element V61() V62() V63() V64() V65() V66() Element of K19(NAT)
{1} is non empty V12() finite V40() 1 -element V61() V62() V63() V64() V65() V66() set
Seg 2 is non empty finite 2 -element V61() V62() V63() V64() V65() V66() Element of K19(NAT)
{1,2} is non empty finite V40() V61() V62() V63() V64() V65() V66() set
0 is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty V17() V21() V22() V23() ext-real non negative V33() V34() finite finite-yielding V40() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V51() V52() V53() V54() V61() V62() V63() V64() V65() V66() V67() Function-yielding V73() Element of NAT
card {} is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty V17() V21() V22() V23() ext-real non negative V33() finite finite-yielding V40() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V51() V52() V53() V54() V61() V62() V63() V64() V65() V66() V67() Function-yielding V73() set
t is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
u is set
Coim (t,u) is set
{u} is non empty V12() finite 1 -element set
t " {u} is finite set
t is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
u is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
c₃ is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
t ^ c₃ is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
u ^ c₃ is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
n is set
Coim (t,n) is finite set
{n} is non empty V12() finite 1 -element set
t " {n} is finite set
card (Coim (t,n)) is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
Coim (u,n) is finite set
u " {n} is finite set
card (Coim (u,n)) is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
Coim ((t ^ c₃),n) is finite set
(t ^ c₃) " {n} is finite set
card (Coim ((t ^ c₃),n)) is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
Coim (c₃,n) is finite set
c₃ " {n} is finite set
card (Coim (c₃,n)) is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
(card (Coim (u,n))) + (card (Coim (c₃,n))) is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
Coim ((u ^ c₃),n) is finite set
(u ^ c₃) " {n} is finite set
card (Coim ((u ^ c₃),n)) is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
n is set
Coim ((t ^ c₃),n) is finite set
{n} is non empty V12() finite 1 -element set
(t ^ c₃) " {n} is finite set
card (Coim ((t ^ c₃),n)) is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
Coim (t,n) is finite set
t " {n} is finite set
card (Coim (t,n)) is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
Coim (c₃,n) is finite set
c₃ " {n} is finite set
card (Coim (c₃,n)) is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
(card (Coim (t,n))) + (card (Coim (c₃,n))) is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
Coim ((u ^ c₃),n) is finite set
(u ^ c₃) " {n} is finite set
card (Coim ((u ^ c₃),n)) is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
Coim (u,n) is finite set
u " {n} is finite set
card (Coim (u,n)) is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
(card (Coim (u,n))) + (card (Coim (c₃,n))) is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
t is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
u is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
t ^ u is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
u ^ t is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
c₃ is set
Coim ((t ^ u),c₃) is finite set
{c₃} is non empty V12() finite 1 -element set
(t ^ u) " {c₃} is finite set
card (Coim ((t ^ u),c₃)) is V17() V21() V22() V23() ext-real non negative V33() finite cardinal set
Coim ((u ^ t),c₃) is finite set
(u ^ t) " {c₃} is finite set
card (Coim ((u ^ t),c₃)) is V17() V21() V22() V23() ext-real non negative V33() finite cardinal set
card (Coim ((t ^ u),c₃)) is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
u " {c₃} is finite set
card (u " {c₃}) is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
t " {c₃} is finite set
card (t " {c₃}) is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
(card (u " {c₃})) + (card (t " {c₃})) is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
card (Coim ((u ^ t),c₃)) is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
t is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
u is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len t is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
len u is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
dom t is finite V61() V62() V63() V64() V65() V66() Element of K19(NAT)
dom u is finite V61() V62() V63() V64() V65() V66() Element of K19(NAT)
Seg (len t) is finite len t -element V61() V62() V63() V64() V65() V66() Element of K19(NAT)
rng t is finite set
t " (rng t) is finite set
card (t " (rng t)) is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
u " (rng t) is finite set
card (u " (rng t)) is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
rng u is finite set
Seg (len u) is finite len u -element V61() V62() V63() V64() V65() V66() Element of K19(NAT)
card (Seg (len t)) is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
u " (rng u) is finite set
card (u " (rng u)) is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
card (Seg (len u)) is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
t is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
u is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
dom u is finite V61() V62() V63() V64() V65() V66() Element of K19(NAT)
K20((dom u),(dom u)) is Relation-like RAT -valued INT -valued finite V51() V52() V53() V54() set
K19(K20((dom u),(dom u))) is finite V40() set
dom t is finite V61() V62() V63() V64() V65() V66() Element of K19(NAT)
c₃ is Relation-like dom u -defined dom u -valued Function-like quasi_total bijective finite V51() V52() V53() V54() Element of K19(K20((dom u),(dom u)))
c₃ * u is Relation-like dom u -defined Function-like finite set
rng c₃ is finite V61() V62() V63() V64() V65() V66() Element of K19(REAL)
dom c₃ is finite V61() V62() V63() V64() V65() V66() Element of K19((dom u))
K19((dom u)) is finite V40() set
dom t is finite V61() V62() V63() V64() V65() V66() Element of K19(NAT)
t is finite set
u is Relation-like Function-like set
u | t is Relation-like Function-like finite set
dom (u | t) is finite set
card (dom (u | t)) is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
c₃ is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty V17() V21() V22() V23() ext-real non negative V33() finite finite-yielding V40() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V51() V52() V53() V54() V61() V62() V63() V64() V65() V66() V67() Function-yielding V73() set
n is set
Coim ((u | t),n) is set
{n} is non empty V12() finite 1 -element set
(u | t) " {n} is finite set
card (Coim ((u | t),n)) is V17() cardinal set
Coim (c₃,n) is finite set
c₃ " {n} is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty V17() V21() V22() V23() ext-real non negative V33() finite finite-yielding V40() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V51() V52() V53() V54() V61() V62() V63() V64() V65() V66() V67() Function-yielding V73() set
card (Coim (c₃,n)) is V17() V21() V22() V23() ext-real non negative V33() finite cardinal set
card (Coim (c₃,n)) is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
t is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
t + 1 is non empty V17() V21() V22() V23() ext-real positive non negative V33() finite cardinal Element of REAL
u is finite set
c₃ is Relation-like Function-like set
c₃ | u is Relation-like Function-like finite set
dom (c₃ | u) is finite set
card (dom (c₃ | u)) is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
n is finite set
the Element of n is Element of n
{ the Element of n} is non empty V12() finite 1 -element set
u \ { the Element of n} is finite Element of K19(u)
K19(u) is finite V40() set
c₃ | (u \ { the Element of n}) is Relation-like Function-like finite set
dom (c₃ | (u \ { the Element of n})) is finite set
dom c₃ is set
(dom c₃) /\ (u \ { the Element of n}) is finite Element of K19(u)
(dom c₃) /\ u is finite set
n \ { the Element of n} is finite Element of K19(n)
K19(n) is finite V40() set
r2 is set
r2 is set
card (dom (c₃ | (u \ { the Element of n}))) is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
card n is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
card { the Element of n} is non empty V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
(card n) - (card { the Element of n}) is V22() V23() ext-real V33() set
(t + 1) - 1 is V22() V23() ext-real V33() Element of REAL
r2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
c₃ . the Element of n is set
<*(c₃ . the Element of n)*> is Relation-like NAT -defined Function-like constant non empty V12() finite 1 -element FinSequence-like FinSubsequence-like set
r2 ^ <*(c₃ . the Element of n)*> is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set
s1 is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set
r1 is set
{r1} is non empty V12() finite 1 -element set
(c₃ | (u \ { the Element of n})) " {r1} is finite set
c₃ | { the Element of n} is Relation-like Function-like finite set
(c₃ | { the Element of n}) " {r1} is finite set
((c₃ | (u \ { the Element of n})) " {r1}) \/ ((c₃ | { the Element of n}) " {r1}) is finite set
c₃ " {r1} is set
(u \ { the Element of n}) /\ (c₃ " {r1}) is finite Element of K19(u)
((u \ { the Element of n}) /\ (c₃ " {r1})) \/ ((c₃ | { the Element of n}) " {r1}) is finite set
{ the Element of n} /\ (c₃ " {r1}) is finite set
((u \ { the Element of n}) /\ (c₃ " {r1})) \/ ({ the Element of n} /\ (c₃ " {r1})) is finite set
(u \ { the Element of n}) \/ { the Element of n} is non empty finite set
((u \ { the Element of n}) \/ { the Element of n}) /\ (c₃ " {r1}) is finite set
u \/ { the Element of n} is non empty finite set
(u \/ { the Element of n}) /\ (c₃ " {r1}) is finite set
u /\ (c₃ " {r1}) is finite set
(c₃ | u) " {r1} is finite set
<*(c₃ . the Element of n)*> " {r1} is finite set
Coim ((c₃ | (u \ { the Element of n})),r1) is set
card (Coim ((c₃ | (u \ { the Element of n})),r1)) is V17() cardinal set
Coim (r2,r1) is finite set
r2 " {r1} is finite set
card (Coim (r2,r1)) is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
dom (c₃ | { the Element of n}) is finite set
dom <*(c₃ . the Element of n)*> is non empty V12() finite 1 -element V61() V62() V63() V64() V65() V66() Element of K19(NAT)
p2 is set
(c₃ | { the Element of n}) . p2 is set
card ((c₃ | { the Element of n}) " {r1}) is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
p2 is set
<*(c₃ . the Element of n)*> . p2 is set
m2 is finite set
card m2 is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
the Element of <*(c₃ . the Element of n)*> " {r1} is Element of <*(c₃ . the Element of n)*> " {r1}
<*(c₃ . the Element of n)*> . the Element of <*(c₃ . the Element of n)*> " {r1} is set
the Element of (c₃ | { the Element of n}) " {r1} is Element of (c₃ | { the Element of n}) " {r1}
(c₃ | { the Element of n}) . the Element of (c₃ | { the Element of n}) " {r1} is set
card ((c₃ | { the Element of n}) " {r1}) is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
m2 is finite set
card m2 is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
card ((c₃ | { the Element of n}) " {r1}) is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
m2 is finite set
card m2 is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
card ((c₃ | { the Element of n}) " {r1}) is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
m2 is finite set
card m2 is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
((c₃ | (u \ { the Element of n})) " {r1}) /\ ((c₃ | { the Element of n}) " {r1}) is finite set
((u \ { the Element of n}) /\ (c₃ " {r1})) /\ ((c₃ | { the Element of n}) " {r1}) is finite Element of K19(u)
((u \ { the Element of n}) /\ (c₃ " {r1})) /\ ({ the Element of n} /\ (c₃ " {r1})) is finite Element of K19(u)
(c₃ " {r1}) /\ (u \ { the Element of n}) is finite Element of K19(u)
((c₃ " {r1}) /\ (u \ { the Element of n})) /\ { the Element of n} is finite Element of K19(u)
(((c₃ " {r1}) /\ (u \ { the Element of n})) /\ { the Element of n}) /\ (c₃ " {r1}) is finite Element of K19(u)
(u \ { the Element of n}) /\ { the Element of n} is finite Element of K19(u)
(c₃ " {r1}) /\ ((u \ { the Element of n}) /\ { the Element of n}) is finite Element of K19(u)
((c₃ " {r1}) /\ ((u \ { the Element of n}) /\ { the Element of n})) /\ (c₃ " {r1}) is finite Element of K19(u)
{} /\ (c₃ " {r1}) is Relation-like finite V61() V62() V63() V64() V65() V66() set
Coim ((c₃ | u),r1) is set
card (Coim ((c₃ | u),r1)) is V17() cardinal set
card ((c₃ | (u \ { the Element of n})) " {r1}) is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
(card ((c₃ | (u \ { the Element of n})) " {r1})) + (card m2) is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
card {} is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty V17() V21() V22() V23() ext-real non negative V33() V34() finite finite-yielding V40() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V51() V52() V53() V54() V61() V62() V63() V64() V65() V66() V67() Function-yielding V73() Element of NAT
((card ((c₃ | (u \ { the Element of n})) " {r1})) + (card m2)) - (card {}) is V22() V23() ext-real V33() Element of REAL
Coim (s1,r1) is finite set
s1 " {r1} is finite set
card (Coim (s1,r1)) is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
t is Relation-like Function-like set
u is finite set
t | u is Relation-like Function-like finite set
dom (t | u) is finite set
card (dom (t | u)) is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
t is V17() V21() V22() V23() ext-real non negative V33() finite cardinal set
u is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len u is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
(len u) - t is V22() V23() ext-real V33() Element of REAL
c₃ is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
n is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len n is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
dom n is finite V61() V62() V63() V64() V65() V66() Element of K19(NAT)
j is V17() V21() V22() V23() ext-real non negative V33() finite cardinal set
n . j is set
j + t is V17() V21() V22() V23() ext-real non negative V33() finite cardinal set
u . (j + t) is set
c₃ is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len c₃ is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
dom c₃ is finite V61() V62() V63() V64() V65() V66() Element of K19(NAT)
n is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len n is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
dom n is finite V61() V62() V63() V64() V65() V66() Element of K19(NAT)
Seg (len c₃) is finite len c₃ -element V61() V62() V63() V64() V65() V66() Element of K19(NAT)
Seg (len n) is finite len n -element V61() V62() V63() V64() V65() V66() Element of K19(NAT)
j is V17() V21() V22() V23() ext-real non negative V33() finite cardinal set
c₃ . j is set
j + t is V17() V21() V22() V23() ext-real non negative V33() finite cardinal set
u . (j + t) is set
n . j is set
t is set
u is V17() V21() V22() V23() ext-real non negative V33() finite cardinal set
c₃ is Relation-like NAT -defined t -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of t
(u,c₃) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len c₃ is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
(len c₃) - u is V22() V23() ext-real V33() Element of REAL
len (u,c₃) is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
j is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
rng (u,c₃) is finite set
rng c₃ is finite Element of K19(t)
K19(t) is set
m3 is set
dom (u,c₃) is finite V61() V62() V63() V64() V65() V66() Element of K19(NAT)
s2 is V17() V21() V22() V23() ext-real non negative V33() finite cardinal set
(u,c₃) . s2 is set
s2 + u is V17() V21() V22() V23() ext-real non negative V33() finite cardinal set
dom c₃ is finite V61() V62() V63() V64() V65() V66() Element of K19(NAT)
c₃ . (s2 + u) is set
len c₃ is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
<*> t is Relation-like non-empty empty-yielding NAT -defined t -valued Function-like one-to-one constant functional empty V17() V21() V22() V23() ext-real non negative V33() finite finite-yielding V40() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V51() V52() V53() V54() V61() V62() V63() V64() V65() V66() V67() Function-yielding V73() FinSequence of t
len c₃ is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
t is V17() V21() V22() V23() ext-real non negative V33() finite cardinal set
u is non empty set
c₃ is Relation-like NAT -defined u -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of u
len c₃ is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
c₃ | t is Relation-like NAT -defined u -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of u
dom c₃ is finite V61() V62() V63() V64() V65() V66() Element of K19(NAT)
Seg (len c₃) is finite len c₃ -element V61() V62() V63() V64() V65() V66() Element of K19(NAT)
Seg t is finite t -element V61() V62() V63() V64() V65() V66() Element of K19(NAT)
c₃ | (Seg t) is Relation-like NAT -defined Seg t -defined NAT -defined u -valued Function-like finite FinSubsequence-like Element of K19(K20(NAT,u))
K20(NAT,u) is Relation-like V12() non finite set
K19(K20(NAT,u)) is V12() non finite set
t is non empty set
u is Relation-like NAT -defined t -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of t
dom u is finite V61() V62() V63() V64() V65() V66() Element of K19(NAT)
c₃ is V17() V21() V22() V23() ext-real non negative V33() finite cardinal set
n is V17() V21() V22() V23() ext-real non negative V33() finite cardinal set
Seg c₃ is finite c₃ -element V61() V62() V63() V64() V65() V66() Element of K19(NAT)
u | c₃ is Relation-like NAT -defined t -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of t
(u | c₃) . n is set
u . n is set
u | (Seg c₃) is Relation-like NAT -defined Seg c₃ -defined NAT -defined t -valued Function-like finite FinSubsequence-like Element of K19(K20(NAT,t))
K20(NAT,t) is Relation-like V12() non finite set
K19(K20(NAT,t)) is V12() non finite set
len u is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
Seg (len u) is finite len u -element V61() V62() V63() V64() V65() V66() Element of K19(NAT)
(dom u) /\ (Seg c₃) is finite V61() V62() V63() V64() V65() V66() Element of K19(NAT)
dom (u | c₃) is finite V61() V62() V63() V64() V65() V66() Element of K19(NAT)
t is non empty set
u is Relation-like NAT -defined t -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of t
len u is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
c₃ is V17() V21() V22() V23() ext-real non negative V33() finite cardinal set
c₃ + 1 is non empty V17() V21() V22() V23() ext-real positive non negative V33() finite cardinal Element of REAL
u . (c₃ + 1) is set
u | c₃ is Relation-like NAT -defined t -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of t
n is set
<*n*> is Relation-like NAT -defined Function-like constant non empty V12() finite 1 -element FinSequence-like FinSubsequence-like set
(u | c₃) ^ <*n*> is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set
len (u | c₃) is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
dom u is finite V61() V62() V63() V64() V65() V66() Element of K19(NAT)
Seg (len u) is finite len u -element V61() V62() V63() V64() V65() V66() Element of K19(NAT)
m3 is V17() V21() V22() V23() ext-real non negative V33() finite cardinal set
u . m3 is set
((u | c₃) ^ <*n*>) . m3 is set
Seg (len (u | c₃)) is finite len (u | c₃) -element V61() V62() V63() V64() V65() V66() Element of K19(NAT)
dom (u | c₃) is finite V61() V62() V63() V64() V65() V66() Element of K19(NAT)
((u | c₃) ^ <*n*>) . m3 is set
(u | c₃) . m3 is set
u . m3 is set
u . m3 is set
((u | c₃) ^ <*n*>) . m3 is set
u . m3 is set
((u | c₃) ^ <*n*>) . m3 is set
len ((u | c₃) ^ <*n*>) is non empty V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
len <*n*> is non empty V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
c₃ + (len <*n*>) is non empty V17() V21() V22() V23() ext-real non negative V33() finite cardinal Element of REAL
t is non empty set
u is Relation-like NAT -defined t -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of t
c₃ is V17() V21() V22() V23() ext-real non negative V33() finite cardinal set
u | c₃ is Relation-like NAT -defined t -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of t
(t,c₃,u) is Relation-like NAT -defined t -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of t
(u | c₃) ^ (t,c₃,u) is Relation-like NAT -defined t -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of t
len u is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
<*> t is Relation-like non-empty empty-yielding NAT -defined t -valued Function-like one-to-one constant functional empty V17() V21() V22() V23() ext-real non negative V33() finite finite-yielding V40() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V51() V52() V53() V54() V61() V62() V63() V64() V65() V66() V67() Function-yielding V73() FinSequence of t
len u is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
dom u is finite V61() V62() V63() V64() V65() V66() Element of K19(NAT)
Seg (len u) is finite len u -element V61() V62() V63() V64() V65() V66() Element of K19(NAT)
len (u | c₃) is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
len (t,c₃,u) is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
(len u) - c₃ is V22() V23() ext-real V33() Element of REAL
len ((u | c₃) ^ (t,c₃,u)) is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
c₃ + ((len u) - c₃) is V22() V23() ext-real V33() Element of REAL
dom (u | c₃) is finite V61() V62() V63() V64() V65() V66() Element of K19(NAT)
Seg c₃ is finite c₃ -element V61() V62() V63() V64() V65() V66() Element of K19(NAT)
j is V17() V21() V22() V23() ext-real non negative V33() finite cardinal set
((u | c₃) ^ (t,c₃,u)) . j is set
(u | c₃) . j is set
u . j is set
j - c₃ is V22() V23() ext-real V33() set
max (0,(j - c₃)) is V22() V23() ext-real set
c₃ + 1 is non empty V17() V21() V22() V23() ext-real positive non negative V33() finite cardinal Element of REAL
m3 is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
dom (t,c₃,u) is finite V61() V62() V63() V64() V65() V66() Element of K19(NAT)
((u | c₃) ^ (t,c₃,u)) . j is set
(t,c₃,u) . m3 is set
m3 + c₃ is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
u . (m3 + c₃) is set
u . j is set
((u | c₃) ^ (t,c₃,u)) . j is set
u . j is set
((u | c₃) ^ (t,c₃,u)) . j is set
u . j is set
len u is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
len u is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
t is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of REAL
u is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of REAL
Sum t is V22() V23() ext-real Element of REAL
K177() is Relation-like K20(REAL,REAL) -defined REAL -valued Function-like quasi_total V51() V52() V53() Element of K19(K20(K20(REAL,REAL),REAL))
K240(REAL,t,K177()) is V22() V23() ext-real Element of REAL
Sum u is V22() V23() ext-real Element of REAL
K240(REAL,u,K177()) is V22() V23() ext-real Element of REAL
len t is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
c₃ is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
c₃ + 1 is non empty V17() V21() V22() V23() ext-real positive non negative V33() finite cardinal Element of REAL
n is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of REAL
j is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of REAL
len n is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
Sum n is V22() V23() ext-real Element of REAL
K240(REAL,n,K177()) is V22() V23() ext-real Element of REAL
Sum j is V22() V23() ext-real Element of REAL
K240(REAL,j,K177()) is V22() V23() ext-real Element of REAL
n . (c₃ + 1) is V22() V23() ext-real Element of REAL
rng n is finite V61() V62() V63() Element of K19(REAL)
rng j is finite V61() V62() V63() Element of K19(REAL)
0 + 1 is non empty V17() V21() V22() V23() ext-real positive non negative V33() finite cardinal Element of REAL
dom n is finite V61() V62() V63() V64() V65() V66() Element of K19(NAT)
dom j is finite V61() V62() V63() V64() V65() V66() Element of K19(NAT)
s2 is V17() V21() V22() V23() ext-real non negative V33() finite cardinal set
j . s2 is V22() V23() ext-real Element of REAL
(REAL,s2,j) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of REAL
j | s2 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of REAL
len j is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
len (j | s2) is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
s2 - 1 is V22() V23() ext-real V33() Element of REAL
max (0,(s2 - 1)) is V22() V23() ext-real set
r1 is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
r1 + 1 is non empty V17() V21() V22() V23() ext-real positive non negative V33() finite cardinal Element of REAL
Seg r1 is finite r1 -element V61() V62() V63() V64() V65() V66() Element of K19(NAT)
Seg s2 is finite s2 -element V61() V62() V63() V64() V65() V66() Element of K19(NAT)
(j | s2) . s2 is V22() V23() ext-real Element of REAL
(j | s2) | r1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of REAL
<*(n . (c₃ + 1))*> is Relation-like NAT -defined REAL -valued Function-like one-to-one constant non empty V12() finite 1 -element FinSequence-like FinSubsequence-like V51() V52() V53() V55() decreasing non-decreasing non-increasing FinSequence of REAL
((j | s2) | r1) ^ <*(n . (c₃ + 1))*> is Relation-like NAT -defined REAL -valued Function-like non empty finite FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of REAL
n | c₃ is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of REAL
(j | s2) ^ (REAL,s2,j) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of REAL
(j | s2) | (Seg r1) is Relation-like NAT -defined Seg r1 -defined NAT -defined REAL -valued Function-like finite FinSubsequence-like V51() V52() V53() Element of K19(K20(NAT,REAL))
K20(NAT,REAL) is Relation-like V12() non finite V51() V52() V53() set
K19(K20(NAT,REAL)) is V12() non finite set
j | (Seg s2) is Relation-like NAT -defined Seg s2 -defined NAT -defined REAL -valued Function-like finite FinSubsequence-like V51() V52() V53() Element of K19(K20(NAT,REAL))
(j | (Seg s2)) | (Seg r1) is Relation-like NAT -defined Seg r1 -defined NAT -defined REAL -valued Function-like finite FinSubsequence-like V51() V52() V53() Element of K19(K20(NAT,REAL))
(Seg s2) /\ (Seg r1) is finite V61() V62() V63() V64() V65() V66() Element of K19(NAT)
j | ((Seg s2) /\ (Seg r1)) is Relation-like NAT -defined (Seg s2) /\ (Seg r1) -defined NAT -defined REAL -valued Function-like finite FinSubsequence-like V51() V52() V53() Element of K19(K20(NAT,REAL))
j | (Seg r1) is Relation-like NAT -defined Seg r1 -defined NAT -defined REAL -valued Function-like finite FinSubsequence-like V51() V52() V53() Element of K19(K20(NAT,REAL))
j | r1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of REAL
(n | c₃) ^ <*(n . (c₃ + 1))*> is Relation-like NAT -defined REAL -valued Function-like non empty finite FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of REAL
p2 is set
Coim (n,p2) is finite set
{p2} is non empty V12() finite 1 -element set
n " {p2} is finite set
card (Coim (n,p2)) is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
Coim (j,p2) is finite set
j " {p2} is finite set
card (Coim (j,p2)) is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
(n | c₃) " {p2} is finite V61() V62() V63() V64() V65() V66() Element of K19(NAT)
card ((n | c₃) " {p2}) is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
<*(n . (c₃ + 1))*> " {p2} is finite V61() V62() V63() V64() V65() V66() Element of K19(NAT)
card (<*(n . (c₃ + 1))*> " {p2}) is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
(card ((n | c₃) " {p2})) + (card (<*(n . (c₃ + 1))*> " {p2})) is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
(j | r1) ^ <*(n . (c₃ + 1))*> is Relation-like NAT -defined REAL -valued Function-like non empty finite FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of REAL
((j | r1) ^ <*(n . (c₃ + 1))*>) ^ (REAL,s2,j) is Relation-like NAT -defined REAL -valued Function-like non empty finite FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of REAL
(((j | r1) ^ <*(n . (c₃ + 1))*>) ^ (REAL,s2,j)) " {p2} is finite V61() V62() V63() V64() V65() V66() Element of K19(NAT)
card ((((j | r1) ^ <*(n . (c₃ + 1))*>) ^ (REAL,s2,j)) " {p2}) is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
((j | r1) ^ <*(n . (c₃ + 1))*>) " {p2} is finite V61() V62() V63() V64() V65() V66() Element of K19(NAT)
card (((j | r1) ^ <*(n . (c₃ + 1))*>) " {p2}) is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
(REAL,s2,j) " {p2} is finite V61() V62() V63() V64() V65() V66() Element of K19(NAT)
card ((REAL,s2,j) " {p2}) is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
(card (((j | r1) ^ <*(n . (c₃ + 1))*>) " {p2})) + (card ((REAL,s2,j) " {p2})) is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
(j | r1) " {p2} is finite V61() V62() V63() V64() V65() V66() Element of K19(NAT)
card ((j | r1) " {p2}) is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
(card ((j | r1) " {p2})) + (card (<*(n . (c₃ + 1))*> " {p2})) is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
((card ((j | r1) " {p2})) + (card (<*(n . (c₃ + 1))*> " {p2}))) + (card ((REAL,s2,j) " {p2})) is V17() V21() V22() V23() ext-real non negative V33() finite cardinal Element of REAL
(card ((j | r1) " {p2})) + (card ((REAL,s2,j) " {p2})) is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
((card ((j | r1) " {p2})) + (card ((REAL,s2,j) " {p2}))) + (card (<*(n . (c₃ + 1))*> " {p2})) is V17() V21() V22() V23() ext-real non negative V33() finite cardinal Element of REAL
(j | r1) ^ (REAL,s2,j) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of REAL
((j | r1) ^ (REAL,s2,j)) " {p2} is finite V61() V62() V63() V64() V65() V66() Element of K19(NAT)
card (((j | r1) ^ (REAL,s2,j)) " {p2}) is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
(card (((j | r1) ^ (REAL,s2,j)) " {p2})) + (card (<*(n . (c₃ + 1))*> " {p2})) is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
Coim ((n | c₃),p2) is finite set
(n | c₃) " {p2} is finite set
card (Coim ((n | c₃),p2)) is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
Coim (((j | r1) ^ (REAL,s2,j)),p2) is finite set
((j | r1) ^ (REAL,s2,j)) " {p2} is finite set
card (Coim (((j | r1) ^ (REAL,s2,j)),p2)) is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
len (n | c₃) is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
Sum (n | c₃) is V22() V23() ext-real Element of REAL
K240(REAL,(n | c₃),K177()) is V22() V23() ext-real Element of REAL
Sum ((j | r1) ^ (REAL,s2,j)) is V22() V23() ext-real Element of REAL
K240(REAL,((j | r1) ^ (REAL,s2,j)),K177()) is V22() V23() ext-real Element of REAL
Sum <*(n . (c₃ + 1))*> is V22() V23() ext-real Element of REAL
K240(REAL,<*(n . (c₃ + 1))*>,K177()) is V22() V23() ext-real Element of REAL
(Sum ((j | r1) ^ (REAL,s2,j))) + (Sum <*(n . (c₃ + 1))*>) is V22() V23() ext-real Element of REAL
Sum (j | r1) is V22() V23() ext-real Element of REAL
K240(REAL,(j | r1),K177()) is V22() V23() ext-real Element of REAL
Sum (REAL,s2,j) is V22() V23() ext-real Element of REAL
K240(REAL,(REAL,s2,j),K177()) is V22() V23() ext-real Element of REAL
(Sum (j | r1)) + (Sum (REAL,s2,j)) is V22() V23() ext-real Element of REAL
((Sum (j | r1)) + (Sum (REAL,s2,j))) + (Sum <*(n . (c₃ + 1))*>) is V22() V23() ext-real Element of REAL
(Sum (j | r1)) + (Sum <*(n . (c₃ + 1))*>) is V22() V23() ext-real Element of REAL
((Sum (j | r1)) + (Sum <*(n . (c₃ + 1))*>)) + (Sum (REAL,s2,j)) is V22() V23() ext-real Element of REAL
Sum (j | s2) is V22() V23() ext-real Element of REAL
K240(REAL,(j | s2),K177()) is V22() V23() ext-real Element of REAL
(Sum (j | s2)) + (Sum (REAL,s2,j)) is V22() V23() ext-real Element of REAL
c₃ is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of REAL
n is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of REAL
len c₃ is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
Sum c₃ is V22() V23() ext-real Element of REAL
K240(REAL,c₃,K177()) is V22() V23() ext-real Element of REAL
Sum n is V22() V23() ext-real Element of REAL
K240(REAL,n,K177()) is V22() V23() ext-real Element of REAL
len n is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
<*> REAL is Relation-like non-empty empty-yielding NAT -defined REAL -valued Function-like one-to-one constant functional empty V17() V21() V22() V23() ext-real non negative V33() finite finite-yielding V40() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V51() V52() V53() V54() V61() V62() V63() V64() V65() V66() V67() Function-yielding V73() FinSequence of REAL
t is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of REAL
len t is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
t . (len t) is V22() V23() ext-real Element of REAL
u is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of REAL
len u is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
u . (len u) is V22() V23() ext-real Element of REAL
(len u) - 1 is V22() V23() ext-real V33() Element of REAL
c₃ is V17() V21() V22() V23() ext-real non negative V33() finite cardinal set
u . c₃ is V22() V23() ext-real Element of REAL
t . c₃ is V22() V23() ext-real Element of REAL
c₃ + 1 is non empty V17() V21() V22() V23() ext-real positive non negative V33() finite cardinal Element of REAL
t . (c₃ + 1) is V22() V23() ext-real Element of REAL
(t . c₃) - (t . (c₃ + 1)) is V22() V23() ext-real Element of REAL
0 + 1 is non empty V17() V21() V22() V23() ext-real positive non negative V33() finite cardinal Element of REAL
(len t) - 1 is V22() V23() ext-real V33() Element of REAL
max (0,((len t) - 1)) is V22() V23() ext-real set
u is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
Seg u is finite u -element V61() V62() V63() V64() V65() V66() Element of K19(NAT)
n is V17() V21() V22() V23() ext-real non negative V33() finite cardinal set
t . n is V22() V23() ext-real Element of REAL
n + 1 is non empty V17() V21() V22() V23() ext-real positive non negative V33() finite cardinal Element of REAL
t . (n + 1) is V22() V23() ext-real Element of REAL
(t . n) - (t . (n + 1)) is V22() V23() ext-real Element of REAL
n is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of REAL
dom n is finite V61() V62() V63() V64() V65() V66() Element of K19(NAT)
<*(t . (len t))*> is Relation-like NAT -defined REAL -valued Function-like one-to-one constant non empty V12() finite 1 -element FinSequence-like FinSubsequence-like V51() V52() V53() V55() decreasing non-decreasing non-increasing FinSequence of REAL
n ^ <*(t . (len t))*> is Relation-like NAT -defined REAL -valued Function-like non empty finite FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of REAL
j is Relation-like NAT -defined REAL -valued Function-like non empty finite FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of REAL
len j is non empty V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
j . (len j) is V22() V23() ext-real Element of REAL
(len j) - 1 is V22() V23() ext-real V33() Element of REAL
len n is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
len <*(t . (len t))*> is non empty V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
(len n) + (len <*(t . (len t))*>) is non empty V17() V21() V22() V23() ext-real non negative V33() finite cardinal Element of REAL
u + (len <*(t . (len t))*>) is non empty V17() V21() V22() V23() ext-real non negative V33() finite cardinal Element of REAL
u + 1 is non empty V17() V21() V22() V23() ext-real positive non negative V33() finite cardinal Element of REAL
j . (u + 1) is V22() V23() ext-real Element of REAL
(len n) + 1 is non empty V17() V21() V22() V23() ext-real positive non negative V33() finite cardinal Element of REAL
j . ((len n) + 1) is V22() V23() ext-real Element of REAL
m3 is V17() V21() V22() V23() ext-real non negative V33() finite cardinal set
j . m3 is V22() V23() ext-real Element of REAL
t . m3 is V22() V23() ext-real Element of REAL
m3 + 1 is non empty V17() V21() V22() V23() ext-real positive non negative V33() finite cardinal Element of REAL
t . (m3 + 1) is V22() V23() ext-real Element of REAL
(t . m3) - (t . (m3 + 1)) is V22() V23() ext-real Element of REAL
n . m3 is V22() V23() ext-real Element of REAL
u is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of REAL
len u is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
u . (len u) is V22() V23() ext-real Element of REAL
(len u) - 1 is V22() V23() ext-real V33() Element of REAL
c₃ is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of REAL
len c₃ is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
c₃ . (len c₃) is V22() V23() ext-real Element of REAL
(len c₃) - 1 is V22() V23() ext-real V33() Element of REAL
dom u is finite V61() V62() V63() V64() V65() V66() Element of K19(NAT)
Seg (len t) is finite len t -element V61() V62() V63() V64() V65() V66() Element of K19(NAT)
n is V17() V21() V22() V23() ext-real non negative V33() finite cardinal set
t . n is V22() V23() ext-real Element of REAL
u . n is V22() V23() ext-real Element of REAL
c₃ . n is V22() V23() ext-real Element of REAL
n + 1 is non empty V17() V21() V22() V23() ext-real positive non negative V33() finite cardinal Element of REAL
t . (n + 1) is V22() V23() ext-real Element of REAL
(len t) - 1 is V22() V23() ext-real V33() Element of REAL
u . n is V22() V23() ext-real Element of REAL
(t . n) - (t . (n + 1)) is V22() V23() ext-real Element of REAL
c₃ . n is V22() V23() ext-real Element of REAL
u . n is V22() V23() ext-real Element of REAL
c₃ . n is V22() V23() ext-real Element of REAL
u . n is V22() V23() ext-real Element of REAL
c₃ . n is V22() V23() ext-real Element of REAL
t is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of REAL
len t is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
(t) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of REAL
u is V22() V23() ext-real Element of REAL
<*u*> is Relation-like NAT -defined REAL -valued Function-like one-to-one constant non empty V12() finite 1 -element FinSequence-like FinSubsequence-like V51() V52() V53() V55() decreasing non-decreasing non-increasing FinSequence of REAL
c₃ is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
c₃ + 2 is non empty V17() V21() V22() V23() ext-real positive non negative V33() finite cardinal Element of REAL
c₃ + 1 is non empty V17() V21() V22() V23() ext-real positive non negative V33() finite cardinal Element of REAL
t . (c₃ + 1) is V22() V23() ext-real Element of REAL
t | (c₃ + 1) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of REAL
((t | (c₃ + 1))) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of REAL
(t) | c₃ is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of REAL
((t) | c₃) ^ <*u*> is Relation-like NAT -defined REAL -valued Function-like non empty finite FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of REAL
0 + 1 is non empty V17() V21() V22() V23() ext-real positive non negative V33() finite cardinal Element of REAL
(c₃ + 1) + 1 is non empty V17() V21() V22() V23() ext-real positive non negative V33() finite cardinal Element of REAL
1 + 1 is non empty V17() V21() V22() V23() ext-real positive non negative V33() finite cardinal Element of REAL
c₃ + (1 + 1) is non empty V17() V21() V22() V23() ext-real positive non negative V33() finite cardinal Element of REAL
Seg (len t) is finite len t -element V61() V62() V63() V64() V65() V66() Element of K19(NAT)
dom t is finite V61() V62() V63() V64() V65() V66() Element of K19(NAT)
Seg (c₃ + 2) is non empty finite c₃ + 2 -element V61() V62() V63() V64() V65() V66() Element of K19(NAT)
len (t | (c₃ + 1)) is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
len ((t | (c₃ + 1))) is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
dom ((t | (c₃ + 1))) is finite V61() V62() V63() V64() V65() V66() Element of K19(NAT)
Seg (c₃ + 1) is non empty finite c₃ + 1 -element V61() V62() V63() V64() V65() V66() Element of K19(NAT)
(t | (c₃ + 1)) . (c₃ + 1) is V22() V23() ext-real Element of REAL
((t | (c₃ + 1))) . (c₃ + 1) is V22() V23() ext-real Element of REAL
len ((t) | c₃) is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
Seg (len ((t) | c₃)) is finite len ((t) | c₃) -element V61() V62() V63() V64() V65() V66() Element of K19(NAT)
dom ((t) | c₃) is finite V61() V62() V63() V64() V65() V66() Element of K19(NAT)
len (t) is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
Seg (len (t)) is finite len (t) -element V61() V62() V63() V64() V65() V66() Element of K19(NAT)
dom (t) is finite V61() V62() V63() V64() V65() V66() Element of K19(NAT)
r2 is V17() V21() V22() V23() ext-real non negative V33() finite cardinal set
((t | (c₃ + 1))) . r2 is V22() V23() ext-real Element of REAL
(((t) | c₃) ^ <*u*>) . r2 is V22() V23() ext-real Element of REAL
Seg c₃ is finite c₃ -element V61() V62() V63() V64() V65() V66() Element of K19(NAT)
r2 + 1 is non empty V17() V21() V22() V23() ext-real positive non negative V33() finite cardinal Element of REAL
t . (r2 + 1) is V22() V23() ext-real Element of REAL
t . r2 is V22() V23() ext-real Element of REAL
(len (t)) - 1 is V22() V23() ext-real V33() Element of REAL
((t) | c₃) . r2 is V22() V23() ext-real Element of REAL
(t) . r2 is V22() V23() ext-real Element of REAL
(t . r2) - (t . (r2 + 1)) is V22() V23() ext-real Element of REAL
(((t) | c₃) ^ <*u*>) . r2 is V22() V23() ext-real Element of REAL
(t | (c₃ + 1)) . (r2 + 1) is V22() V23() ext-real Element of REAL
(len ((t | (c₃ + 1)))) - 1 is V22() V23() ext-real V33() Element of REAL
(t | (c₃ + 1)) . r2 is V22() V23() ext-real Element of REAL
((t | (c₃ + 1))) . r2 is V22() V23() ext-real Element of REAL
((t | (c₃ + 1))) . r2 is V22() V23() ext-real Element of REAL
(((t) | c₃) ^ <*u*>) . r2 is V22() V23() ext-real Element of REAL
((t | (c₃ + 1))) . r2 is V22() V23() ext-real Element of REAL
(((t) | c₃) ^ <*u*>) . r2 is V22() V23() ext-real Element of REAL
len (((t) | c₃) ^ <*u*>) is non empty V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
len <*u*> is non empty V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
c₃ + (len <*u*>) is non empty V17() V21() V22() V23() ext-real non negative V33() finite cardinal Element of REAL
t is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of REAL
len t is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
(t) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of REAL
u is V22() V23() ext-real Element of REAL
c₃ is V22() V23() ext-real Element of REAL
u - c₃ is V22() V23() ext-real Element of REAL
<*(u - c₃),c₃*> is Relation-like NAT -defined REAL -valued Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of REAL
n is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
n + 2 is non empty V17() V21() V22() V23() ext-real positive non negative V33() finite cardinal Element of REAL
n + 1 is non empty V17() V21() V22() V23() ext-real positive non negative V33() finite cardinal Element of REAL
t . (n + 1) is V22() V23() ext-real Element of REAL
t . (n + 2) is V22() V23() ext-real Element of REAL
(t) | n is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of REAL
((t) | n) ^ <*(u - c₃),c₃*> is Relation-like NAT -defined REAL -valued Function-like non empty finite FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of REAL
len (t) is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
dom (t) is finite V61() V62() V63() V64() V65() V66() Element of K19(NAT)
Seg (n + 2) is non empty finite n + 2 -element V61() V62() V63() V64() V65() V66() Element of K19(NAT)
1 + 1 is non empty V17() V21() V22() V23() ext-real positive non negative V33() finite cardinal Element of REAL
n + (1 + 1) is non empty V17() V21() V22() V23() ext-real positive non negative V33() finite cardinal Element of REAL
(n + 1) + 1 is non empty V17() V21() V22() V23() ext-real positive non negative V33() finite cardinal Element of REAL
len ((t) | n) is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
len (((t) | n) ^ <*(u - c₃),c₃*>) is non empty V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
len <*(u - c₃),c₃*> is non empty V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
n + (len <*(u - c₃),c₃*>) is non empty V17() V21() V22() V23() ext-real non negative V33() finite cardinal Element of REAL
s2 is V17() V21() V22() V23() ext-real non negative V33() finite cardinal set
(t) . s2 is V22() V23() ext-real Element of REAL
(n + 2) - n is V22() V23() ext-real V33() Element of REAL
<*(u - c₃),c₃*> . ((n + 2) - n) is V22() V23() ext-real Element of REAL
(((t) | n) ^ <*(u - c₃),c₃*>) . s2 is V22() V23() ext-real Element of REAL
(len (t)) - 1 is V22() V23() ext-real V33() Element of REAL
(t) . s2 is V22() V23() ext-real Element of REAL
(n + 1) - n is V22() V23() ext-real V33() Element of REAL
<*(u - c₃),c₃*> . ((n + 1) - n) is V22() V23() ext-real Element of REAL
(((t) | n) ^ <*(u - c₃),c₃*>) . s2 is V22() V23() ext-real Element of REAL
Seg n is finite n -element V61() V62() V63() V64() V65() V66() Element of K19(NAT)
dom ((t) | n) is finite V61() V62() V63() V64() V65() V66() Element of K19(NAT)
Seg (len ((t) | n)) is finite len ((t) | n) -element V61() V62() V63() V64() V65() V66() Element of K19(NAT)
Seg (len (t)) is finite len (t) -element V61() V62() V63() V64() V65() V66() Element of K19(NAT)
(t) . s2 is V22() V23() ext-real Element of REAL
((t) | n) . s2 is V22() V23() ext-real Element of REAL
(((t) | n) ^ <*(u - c₃),c₃*>) . s2 is V22() V23() ext-real Element of REAL
(t) . s2 is V22() V23() ext-real Element of REAL
(((t) | n) ^ <*(u - c₃),c₃*>) . s2 is V22() V23() ext-real Element of REAL
(t) . s2 is V22() V23() ext-real Element of REAL
(((t) | n) ^ <*(u - c₃),c₃*>) . s2 is V22() V23() ext-real Element of REAL
(t) . s2 is V22() V23() ext-real Element of REAL
(((t) | n) ^ <*(u - c₃),c₃*>) . s2 is V22() V23() ext-real Element of REAL
(t) . s2 is V22() V23() ext-real Element of REAL
(((t) | n) ^ <*(u - c₃),c₃*>) . s2 is V22() V23() ext-real Element of REAL
<*> REAL is Relation-like non-empty empty-yielding NAT -defined REAL -valued Function-like one-to-one constant functional empty V17() V21() V22() V23() ext-real non negative V33() finite finite-yielding V40() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V51() V52() V53() V54() V61() V62() V63() V64() V65() V66() V67() Function-yielding V73() FinSequence of REAL
((<*> REAL)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of REAL
len ((<*> REAL)) is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
len (<*> REAL) is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty V17() V21() V22() V23() ext-real non negative V33() V34() finite finite-yielding V40() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V51() V52() V53() V54() V61() V62() V63() V64() V65() V66() V67() Function-yielding V73() Element of NAT
t is V22() V23() ext-real Element of REAL
<*t*> is Relation-like NAT -defined REAL -valued Function-like one-to-one constant non empty V12() finite 1 -element FinSequence-like FinSubsequence-like V51() V52() V53() V55() decreasing non-decreasing non-increasing FinSequence of REAL
(<*t*>) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of REAL
len <*t*> is non empty V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
len (<*t*>) is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
dom (<*t*>) is finite V61() V62() V63() V64() V65() V66() Element of K19(NAT)
c₃ is V17() V21() V22() V23() ext-real non negative V33() finite cardinal set
(<*t*>) . c₃ is V22() V23() ext-real Element of REAL
<*t*> . c₃ is V22() V23() ext-real Element of REAL
t is V22() V23() ext-real Element of REAL
u is V22() V23() ext-real Element of REAL
<*t,u*> is Relation-like NAT -defined REAL -valued Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of REAL
(<*t,u*>) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of REAL
t - u is V22() V23() ext-real Element of REAL
<*(t - u),u*> is Relation-like NAT -defined REAL -valued Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of REAL
len <*t,u*> is non empty V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
<*t,u*> . 1 is V22() V23() ext-real Element of REAL
<*t,u*> . 2 is V22() V23() ext-real Element of REAL
0 + 2 is non empty V17() V21() V22() V23() ext-real positive non negative V33() finite cardinal Element of REAL
0 + 1 is non empty V17() V21() V22() V23() ext-real positive non negative V33() finite cardinal Element of REAL
(<*t,u*>) | 0 is Relation-like non-empty empty-yielding NAT -defined REAL -valued RAT -valued Function-like one-to-one constant functional empty V17() V21() V22() V23() ext-real non negative V33() finite finite-yielding V40() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V51() V52() V53() V54() V61() V62() V63() V64() V65() V66() V67() Function-yielding V73() FinSequence of REAL
((<*t,u*>) | 0) ^ <*(t - u),u*> is Relation-like NAT -defined REAL -valued Function-like non empty finite {} + 2 -element FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of REAL
{} + 2 is non empty V17() V21() V22() V23() ext-real positive non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
t is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of REAL
(t) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of REAL
u is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
(REAL,u,(t)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of REAL
(REAL,u,t) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of REAL
((REAL,u,t)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of REAL
len (t) is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
len t is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
len ((REAL,u,t)) is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
len (REAL,u,t) is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
len (REAL,u,(t)) is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
(len t) - u is V22() V23() ext-real V33() Element of REAL
dom ((REAL,u,t)) is finite V61() V62() V63() V64() V65() V66() Element of K19(NAT)
Seg (len (REAL,u,t)) is finite len (REAL,u,t) -element V61() V62() V63() V64() V65() V66() Element of K19(NAT)
Seg (len (REAL,u,(t))) is finite len (REAL,u,(t)) -element V61() V62() V63() V64() V65() V66() Element of K19(NAT)
dom (REAL,u,(t)) is finite V61() V62() V63() V64() V65() V66() Element of K19(NAT)
dom (REAL,u,t) is finite V61() V62() V63() V64() V65() V66() Element of K19(NAT)
m3 is V17() V21() V22() V23() ext-real non negative V33() finite cardinal set
m3 + u is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
t . (m3 + u) is V22() V23() ext-real Element of REAL
(REAL,u,t) . m3 is V22() V23() ext-real Element of REAL
(REAL,u,(t)) . m3 is V22() V23() ext-real Element of REAL
(t) . (m3 + u) is V22() V23() ext-real Element of REAL
((REAL,u,t)) . m3 is V22() V23() ext-real Element of REAL
m3 + 1 is non empty V17() V21() V22() V23() ext-real positive non negative V33() finite cardinal Element of REAL
(len (REAL,u,t)) - 1 is V22() V23() ext-real V33() Element of REAL
(m3 + 1) + u is non empty V17() V21() V22() V23() ext-real positive non negative V33() finite cardinal Element of REAL
t . ((m3 + 1) + u) is V22() V23() ext-real Element of REAL
(m3 + u) + 1 is non empty V17() V21() V22() V23() ext-real positive non negative V33() finite cardinal Element of REAL
(REAL,u,t) . (m3 + 1) is V22() V23() ext-real Element of REAL
(len t) - 1 is V22() V23() ext-real V33() Element of REAL
(REAL,u,(t)) . m3 is V22() V23() ext-real Element of REAL
(t) . (m3 + u) is V22() V23() ext-real Element of REAL
(t . (m3 + u)) - (t . ((m3 + 1) + u)) is V22() V23() ext-real Element of REAL
((REAL,u,t)) . m3 is V22() V23() ext-real Element of REAL
(REAL,u,(t)) . m3 is V22() V23() ext-real Element of REAL
((REAL,u,t)) . m3 is V22() V23() ext-real Element of REAL
(REAL,u,(t)) . m3 is V22() V23() ext-real Element of REAL
((REAL,u,t)) . m3 is V22() V23() ext-real Element of REAL
t is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of REAL
len t is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
(t) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of REAL
Sum (t) is V22() V23() ext-real Element of REAL
K177() is Relation-like K20(REAL,REAL) -defined REAL -valued Function-like quasi_total V51() V52() V53() Element of K19(K20(K20(REAL,REAL),REAL))
K240(REAL,(t),K177()) is V22() V23() ext-real Element of REAL
t . 1 is V22() V23() ext-real Element of REAL
u is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
u + 1 is non empty V17() V21() V22() V23() ext-real positive non negative V33() finite cardinal Element of REAL
c₃ is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of REAL
len c₃ is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
(c₃) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of REAL
Sum (c₃) is V22() V23() ext-real Element of REAL
K240(REAL,(c₃),K177()) is V22() V23() ext-real Element of REAL
c₃ . 1 is V22() V23() ext-real Element of REAL
<*(c₃ . 1)*> is Relation-like NAT -defined REAL -valued Function-like one-to-one constant non empty V12() finite 1 -element FinSequence-like FinSubsequence-like V51() V52() V53() V55() decreasing non-decreasing non-increasing FinSequence of REAL
0 + 1 is non empty V17() V21() V22() V23() ext-real positive non negative V33() finite cardinal Element of REAL
u - 1 is V22() V23() ext-real V33() Element of REAL
max (0,(u - 1)) is V22() V23() ext-real set
n is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
n + 1 is non empty V17() V21() V22() V23() ext-real positive non negative V33() finite cardinal Element of REAL
Seg (len c₃) is finite len c₃ -element V61() V62() V63() V64() V65() V66() Element of K19(NAT)
dom c₃ is finite V61() V62() V63() V64() V65() V66() Element of K19(NAT)
Seg (n + 1) is non empty finite n + 1 -element V61() V62() V63() V64() V65() V66() Element of K19(NAT)
n + 2 is non empty V17() V21() V22() V23() ext-real positive non negative V33() finite cardinal Element of REAL
(n + 1) + 1 is non empty V17() V21() V22() V23() ext-real positive non negative V33() finite cardinal Element of REAL
Seg (n + 2) is non empty finite n + 2 -element V61() V62() V63() V64() V65() V66() Element of K19(NAT)
c₃ | (n + 1) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of REAL
c₃ . (n + 2) is V22() V23() ext-real Element of REAL
c₃ . (n + 1) is V22() V23() ext-real Element of REAL
len (c₃ | (n + 1)) is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
(c₃) | n is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of REAL
(c₃ . (n + 1)) - (c₃ . (n + 2)) is V22() V23() ext-real Element of REAL
<*((c₃ . (n + 1)) - (c₃ . (n + 2))),(c₃ . (n + 2))*> is Relation-like NAT -defined REAL -valued Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of REAL
((c₃) | n) ^ <*((c₃ . (n + 1)) - (c₃ . (n + 2))),(c₃ . (n + 2))*> is Relation-like NAT -defined REAL -valued Function-like non empty finite FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of REAL
Sum (((c₃) | n) ^ <*((c₃ . (n + 1)) - (c₃ . (n + 2))),(c₃ . (n + 2))*>) is V22() V23() ext-real Element of REAL
K240(REAL,(((c₃) | n) ^ <*((c₃ . (n + 1)) - (c₃ . (n + 2))),(c₃ . (n + 2))*>),K177()) is V22() V23() ext-real Element of REAL
Sum ((c₃) | n) is V22() V23() ext-real Element of REAL
K240(REAL,((c₃) | n),K177()) is V22() V23() ext-real Element of REAL
Sum <*((c₃ . (n + 1)) - (c₃ . (n + 2))),(c₃ . (n + 2))*> is V22() V23() ext-real Element of REAL
K240(REAL,<*((c₃ . (n + 1)) - (c₃ . (n + 2))),(c₃ . (n + 2))*>,K177()) is V22() V23() ext-real Element of REAL
(Sum ((c₃) | n)) + (Sum <*((c₃ . (n + 1)) - (c₃ . (n + 2))),(c₃ . (n + 2))*>) is V22() V23() ext-real Element of REAL
((c₃ . (n + 1)) - (c₃ . (n + 2))) + (c₃ . (n + 2)) is V22() V23() ext-real Element of REAL
(Sum ((c₃) | n)) + (((c₃ . (n + 1)) - (c₃ . (n + 2))) + (c₃ . (n + 2))) is V22() V23() ext-real Element of REAL
<*(c₃ . (n + 1))*> is Relation-like NAT -defined REAL -valued Function-like one-to-one constant non empty V12() finite 1 -element FinSequence-like FinSubsequence-like V51() V52() V53() V55() decreasing non-decreasing non-increasing FinSequence of REAL
((c₃) | n) ^ <*(c₃ . (n + 1))*> is Relation-like NAT -defined REAL -valued Function-like non empty finite FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of REAL
Sum (((c₃) | n) ^ <*(c₃ . (n + 1))*>) is V22() V23() ext-real Element of REAL
K240(REAL,(((c₃) | n) ^ <*(c₃ . (n + 1))*>),K177()) is V22() V23() ext-real Element of REAL
((c₃ | (n + 1))) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of REAL
Sum ((c₃ | (n + 1))) is V22() V23() ext-real Element of REAL
K240(REAL,((c₃ | (n + 1))),K177()) is V22() V23() ext-real Element of REAL
(c₃ | (n + 1)) . 1 is V22() V23() ext-real Element of REAL
u is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of REAL
len u is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
(u) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of REAL
Sum (u) is V22() V23() ext-real Element of REAL
K240(REAL,(u),K177()) is V22() V23() ext-real Element of REAL
u . 1 is V22() V23() ext-real Element of REAL
t is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of REAL
len t is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
u is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
(REAL,u,t) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of REAL
((REAL,u,t)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of REAL
Sum ((REAL,u,t)) is V22() V23() ext-real Element of REAL
K177() is Relation-like K20(REAL,REAL) -defined REAL -valued Function-like quasi_total V51() V52() V53() Element of K19(K20(K20(REAL,REAL),REAL))
K240(REAL,((REAL,u,t)),K177()) is V22() V23() ext-real Element of REAL
u + 1 is non empty V17() V21() V22() V23() ext-real positive non negative V33() finite cardinal Element of REAL
t . (u + 1) is V22() V23() ext-real Element of REAL
len (REAL,u,t) is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
(len t) - u is V22() V23() ext-real V33() Element of REAL
dom (REAL,u,t) is finite V61() V62() V63() V64() V65() V66() Element of K19(NAT)
(REAL,u,t) . 1 is V22() V23() ext-real Element of REAL
t is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of REAL
dom t is finite V61() V62() V63() V64() V65() V66() Element of K19(NAT)
u is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
u + 1 is non empty V17() V21() V22() V23() ext-real positive non negative V33() finite cardinal Element of REAL
t . (u + 1) is V22() V23() ext-real Element of REAL
t . u is V22() V23() ext-real Element of REAL
u + 0 is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
u is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
dom t is finite set
t . u is V22() V23() ext-real Element of REAL
c₃ is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
t . c₃ is V22() V23() ext-real Element of REAL
n is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
t . n is V22() V23() ext-real Element of REAL
n + 1 is non empty V17() V21() V22() V23() ext-real positive non negative V33() finite cardinal Element of REAL
t . (n + 1) is V22() V23() ext-real Element of REAL
n + 0 is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
len t is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
t . 0 is V22() V23() ext-real Element of REAL
t is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
dom (<*> REAL) is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty V17() V21() V22() V23() ext-real non negative V33() finite finite-yielding V40() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V51() V52() V53() V54() V61() V62() V63() V64() V65() V66() V67() Function-yielding V73() Element of K19(NAT)
t + 1 is non empty V17() V21() V22() V23() ext-real positive non negative V33() finite cardinal Element of REAL
(<*> REAL) . (t + 1) is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty V17() V21() V22() V23() ext-real non negative V33() finite finite-yielding V40() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V51() V52() V53() V54() V61() V62() V63() V64() V65() V66() V67() Function-yielding V73() Element of REAL
(<*> REAL) . t is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty V17() V21() V22() V23() ext-real non negative V33() finite finite-yielding V40() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V51() V52() V53() V54() V61() V62() V63() V64() V65() V66() V67() Function-yielding V73() Element of REAL
t is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of REAL
len t is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
dom t is finite V61() V62() V63() V64() V65() V66() Element of K19(NAT)
u is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
u + 1 is non empty V17() V21() V22() V23() ext-real positive non negative V33() finite cardinal Element of REAL
t . (u + 1) is V22() V23() ext-real Element of REAL
t . u is V22() V23() ext-real Element of REAL
dom t is finite V61() V62() V63() V64() V65() V66() Element of K19(NAT)
u is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
u + 1 is non empty V17() V21() V22() V23() ext-real positive non negative V33() finite cardinal Element of REAL
t . (u + 1) is V22() V23() ext-real Element of REAL
t . u is V22() V23() ext-real Element of REAL
t is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of REAL
dom t is finite V61() V62() V63() V64() V65() V66() Element of K19(NAT)
u is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
t . u is V22() V23() ext-real Element of REAL
u + 1 is non empty V17() V21() V22() V23() ext-real positive non negative V33() finite cardinal Element of REAL
t . (u + 1) is V22() V23() ext-real Element of REAL
len t is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
c₃ is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
t . c₃ is V22() V23() ext-real Element of REAL
len t is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
Seg (len t) is finite len t -element V61() V62() V63() V64() V65() V66() Element of K19(NAT)
t . 0 is V22() V23() ext-real Element of REAL
u is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
t . u is V22() V23() ext-real Element of REAL
u is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
c₃ is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
t . c₃ is V22() V23() ext-real Element of REAL
t . u is V22() V23() ext-real Element of REAL
u is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
u + 1 is non empty V17() V21() V22() V23() ext-real positive non negative V33() finite cardinal Element of REAL
t . (u + 1) is V22() V23() ext-real Element of REAL
t . u is V22() V23() ext-real Element of REAL
t is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V51() V52() V53() non-increasing FinSequence of REAL
u is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
t | u is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of REAL
len (t | u) is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
0 + 1 is non empty V17() V21() V22() V23() ext-real positive non negative V33() finite cardinal Element of REAL
len t is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
len t is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
dom t is finite V61() V62() V63() V64() V65() V66() Element of K19(NAT)
len (t | u) is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
dom (t | u) is finite V61() V62() V63() V64() V65() V66() Element of K19(NAT)
Seg (len (t | u)) is finite len (t | u) -element V61() V62() V63() V64() V65() V66() Element of K19(NAT)
n is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
n + 1 is non empty V17() V21() V22() V23() ext-real positive non negative V33() finite cardinal Element of REAL
t . n is V22() V23() ext-real Element of REAL
(t | u) . n is V22() V23() ext-real Element of REAL
t . (n + 1) is V22() V23() ext-real Element of REAL
(t | u) . (n + 1) is V22() V23() ext-real Element of REAL
len t is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
len t is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
t is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V51() V52() V53() non-increasing FinSequence of REAL
u is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
(REAL,u,t) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of REAL
n is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
dom (REAL,u,t) is finite V61() V62() V63() V64() V65() V66() Element of K19(NAT)
n + 1 is non empty V17() V21() V22() V23() ext-real positive non negative V33() finite cardinal Element of REAL
n + u is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
(n + u) + 1 is non empty V17() V21() V22() V23() ext-real positive non negative V33() finite cardinal Element of REAL
len (REAL,u,t) is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
(REAL,u,t) . n is V22() V23() ext-real Element of REAL
(REAL,u,t) . (n + 1) is V22() V23() ext-real Element of REAL
(n + 1) + u is non empty V17() V21() V22() V23() ext-real positive non negative V33() finite cardinal Element of REAL
len t is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
(len t) - u is V22() V23() ext-real V33() Element of REAL
dom t is finite V61() V62() V63() V64() V65() V66() Element of K19(NAT)
t . (n + u) is V22() V23() ext-real Element of REAL
t . ((n + u) + 1) is V22() V23() ext-real Element of REAL
len t is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
len t is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
len t is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
t is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V51() V52() V53() non-increasing FinSequence of REAL
len t is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
u is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V51() V52() V53() non-increasing FinSequence of REAL
len u is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
t . (len t) is V22() V23() ext-real Element of REAL
u . (len u) is V22() V23() ext-real Element of REAL
c₃ is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
c₃ + 1 is non empty V17() V21() V22() V23() ext-real positive non negative V33() finite cardinal Element of REAL
t | c₃ is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of REAL
u | c₃ is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of REAL
t . (c₃ + 1) is V22() V23() ext-real Element of REAL
u . (c₃ + 1) is V22() V23() ext-real Element of REAL
0 + 1 is non empty V17() V21() V22() V23() ext-real positive non negative V33() finite cardinal Element of REAL
dom t is finite V61() V62() V63() V64() V65() V66() Element of K19(NAT)
<*(t . (c₃ + 1))*> is Relation-like NAT -defined REAL -valued Function-like one-to-one constant non empty V12() finite 1 -element FinSequence-like FinSubsequence-like V51() V52() V53() V55() decreasing non-decreasing non-increasing FinSequence of REAL
(t | c₃) ^ <*(t . (c₃ + 1))*> is Relation-like NAT -defined REAL -valued Function-like non empty finite FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of REAL
dom u is finite V61() V62() V63() V64() V65() V66() Element of K19(NAT)
rng t is finite V61() V62() V63() Element of K19(REAL)
rng u is finite V61() V62() V63() Element of K19(REAL)
m3 is V17() V21() V22() V23() ext-real non negative V33() finite cardinal set
t . m3 is V22() V23() ext-real Element of REAL
m3 is V17() V21() V22() V23() ext-real non negative V33() finite cardinal set
u . m3 is V22() V23() ext-real Element of REAL
(u | c₃) ^ <*(t . (c₃ + 1))*> is Relation-like NAT -defined REAL -valued Function-like non empty finite FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of REAL
m3 is set
Coim ((t | c₃),m3) is finite set
{m3} is non empty V12() finite 1 -element set
(t | c₃) " {m3} is finite set
card (Coim ((t | c₃),m3)) is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
<*(t . (c₃ + 1))*> " {m3} is finite V61() V62() V63() V64() V65() V66() Element of K19(NAT)
card (<*(t . (c₃ + 1))*> " {m3}) is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
(card (Coim ((t | c₃),m3))) + (card (<*(t . (c₃ + 1))*> " {m3})) is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
Coim (t,m3) is finite set
t " {m3} is finite set
card (Coim (t,m3)) is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
Coim (u,m3) is finite set
u " {m3} is finite set
card (Coim (u,m3)) is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
Coim ((u | c₃),m3) is finite set
(u | c₃) " {m3} is finite set
card (Coim ((u | c₃),m3)) is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
(card (Coim ((u | c₃),m3))) + (card (<*(t . (c₃ + 1))*> " {m3})) is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
t is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of REAL
len t is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
u is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V51() V52() V53() non-increasing FinSequence of REAL
t is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
t + 1 is non empty V17() V21() V22() V23() ext-real positive non negative V33() finite cardinal Element of REAL
u is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of REAL
len u is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
Seg t is finite t -element V61() V62() V63() V64() V65() V66() Element of K19(NAT)
u | (Seg t) is Relation-like NAT -defined Seg t -defined NAT -defined REAL -valued Function-like finite FinSubsequence-like V51() V52() V53() Element of K19(K20(NAT,REAL))
K20(NAT,REAL) is Relation-like V12() non finite V51() V52() V53() set
K19(K20(NAT,REAL)) is V12() non finite set
u | t is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of REAL
u . (t + 1) is V22() V23() ext-real Element of REAL
j is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
rng j is finite set
rng u is finite V61() V62() V63() Element of K19(REAL)
m3 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of REAL
dom m3 is finite V61() V62() V63() V64() V65() V66() Element of K19(NAT)
dom u is finite V61() V62() V63() V64() V65() V66() Element of K19(NAT)
(dom u) /\ (Seg t) is finite V61() V62() V63() V64() V65() V66() Element of K19(NAT)
Seg (t + 1) is non empty finite t + 1 -element V61() V62() V63() V64() V65() V66() Element of K19(NAT)
len m3 is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
s2 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V51() V52() V53() non-increasing FinSequence of REAL
len s2 is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
Seg (len s2) is finite len s2 -element V61() V62() V63() V64() V65() V66() Element of K19(NAT)
dom s2 is finite V61() V62() V63() V64() V65() V66() Element of K19(NAT)
rng s2 is finite V61() V62() V63() Element of K19(REAL)
<*(u . (t + 1))*> is Relation-like NAT -defined REAL -valued Function-like one-to-one constant non empty V12() finite 1 -element FinSequence-like FinSubsequence-like V51() V52() V53() V55() decreasing non-decreasing non-increasing FinSequence of REAL
s2 ^ <*(u . (t + 1))*> is Relation-like NAT -defined REAL -valued Function-like non empty finite FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of REAL
len (s2 ^ <*(u . (t + 1))*>) is non empty V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
len <*(u . (t + 1))*> is non empty V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
t + (len <*(u . (t + 1))*>) is non empty V17() V21() V22() V23() ext-real non negative V33() finite cardinal Element of REAL
s1 is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
dom (s2 ^ <*(u . (t + 1))*>) is non empty finite V61() V62() V63() V64() V65() V66() Element of K19(NAT)
s1 + 1 is non empty V17() V21() V22() V23() ext-real positive non negative V33() finite cardinal Element of REAL
(s2 ^ <*(u . (t + 1))*>) . s1 is V22() V23() ext-real Element of REAL
(s2 ^ <*(u . (t + 1))*>) . (s1 + 1) is V22() V23() ext-real Element of REAL
(t + 1) - 1 is V22() V23() ext-real V33() Element of REAL
s2 . s1 is V22() V23() ext-real Element of REAL
s2 . (s1 + 1) is V22() V23() ext-real Element of REAL
s1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V51() V52() V53() non-increasing FinSequence of REAL
m3 ^ <*(u . (t + 1))*> is Relation-like NAT -defined REAL -valued Function-like non empty finite FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of REAL
r1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V51() V52() V53() non-increasing FinSequence of REAL
rng s2 is finite V61() V62() V63() Element of K19(REAL)
r2 is V22() V23() ext-real Element of REAL
r2 is V22() V23() ext-real Element of REAL
s1 is V17() V21() V22() V23() ext-real non negative V33() finite cardinal set
s2 . s1 is V22() V23() ext-real Element of REAL
r1 is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
s2 . r1 is V22() V23() ext-real Element of REAL
m2 is V22() V23() ext-real Element of REAL
r2 is V17() V21() V22() V23() ext-real non negative V33() finite cardinal set
s2 . r2 is V22() V23() ext-real Element of REAL
r2 - 1 is V22() V23() ext-real V33() Element of REAL
max (0,(r2 - 1)) is V22() V23() ext-real set
r2 + 1 is non empty V17() V21() V22() V23() ext-real positive non negative V33() finite cardinal Element of REAL
s1 is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
(REAL,s1,s2) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of REAL
len (REAL,s1,s2) is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
(len s2) - s1 is V22() V23() ext-real V33() Element of REAL
s2 | s1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of REAL
<*(u . (t + 1))*> is Relation-like NAT -defined REAL -valued Function-like one-to-one constant non empty V12() finite 1 -element FinSequence-like FinSubsequence-like V51() V52() V53() V55() decreasing non-decreasing non-increasing FinSequence of REAL
(s2 | s1) ^ <*(u . (t + 1))*> is Relation-like NAT -defined REAL -valued Function-like non empty finite FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of REAL
dom ((s2 | s1) ^ <*(u . (t + 1))*>) is non empty finite V61() V62() V63() V64() V65() V66() Element of K19(NAT)
len ((s2 | s1) ^ <*(u . (t + 1))*>) is non empty V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
Seg (len ((s2 | s1) ^ <*(u . (t + 1))*>)) is non empty finite len ((s2 | s1) ^ <*(u . (t + 1))*>) -element V61() V62() V63() V64() V65() V66() Element of K19(NAT)
dom (s2 | s1) is finite V61() V62() V63() V64() V65() V66() Element of K19(NAT)
((s2 | s1) ^ <*(u . (t + 1))*>) ^ (REAL,s1,s2) is Relation-like NAT -defined REAL -valued Function-like non empty finite FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of REAL
len (s2 | s1) is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
Seg (len (s2 | s1)) is finite len (s2 | s1) -element V61() V62() V63() V64() V65() V66() Element of K19(NAT)
len <*(u . (t + 1))*> is non empty V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
s1 + (len <*(u . (t + 1))*>) is non empty V17() V21() V22() V23() ext-real non negative V33() finite cardinal Element of REAL
s1 + 1 is non empty V17() V21() V22() V23() ext-real positive non negative V33() finite cardinal Element of REAL
len (((s2 | s1) ^ <*(u . (t + 1))*>) ^ (REAL,s1,s2)) is non empty V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
(s1 + 1) + (len (REAL,s1,s2)) is non empty V17() V21() V22() V23() ext-real positive non negative V33() finite cardinal Element of REAL
p2 is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
dom (((s2 | s1) ^ <*(u . (t + 1))*>) ^ (REAL,s1,s2)) is non empty finite V61() V62() V63() V64() V65() V66() Element of K19(NAT)
p2 + 1 is non empty V17() V21() V22() V23() ext-real positive non negative V33() finite cardinal Element of REAL
(((s2 | s1) ^ <*(u . (t + 1))*>) ^ (REAL,s1,s2)) . p2 is V22() V23() ext-real Element of REAL
(((s2 | s1) ^ <*(u . (t + 1))*>) ^ (REAL,s1,s2)) . (p2 + 1) is V22() V23() ext-real Element of REAL
(s2 | s1) ^ (REAL,s1,s2) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of REAL
dom ((s2 | s1) ^ (REAL,s1,s2)) is finite V61() V62() V63() V64() V65() V66() Element of K19(NAT)
Seg s1 is finite s1 -element V61() V62() V63() V64() V65() V66() Element of K19(NAT)
s2 . p2 is V22() V23() ext-real Element of REAL
(s2 | s1) . p2 is V22() V23() ext-real Element of REAL
s2 . (p2 + 1) is V22() V23() ext-real Element of REAL
(s2 | s1) . (p2 + 1) is V22() V23() ext-real Element of REAL
((s2 | s1) ^ <*(u . (t + 1))*>) . (p2 + 1) is V22() V23() ext-real Element of REAL
((s2 | s1) ^ <*(u . (t + 1))*>) . p2 is V22() V23() ext-real Element of REAL
((s2 | s1) ^ <*(u . (t + 1))*>) . (s1 + 1) is V22() V23() ext-real Element of REAL
Seg s1 is finite s1 -element V61() V62() V63() V64() V65() V66() Element of K19(NAT)
s2 . p2 is V22() V23() ext-real Element of REAL
(s2 | s1) . p2 is V22() V23() ext-real Element of REAL
((s2 | s1) ^ <*(u . (t + 1))*>) . p2 is V22() V23() ext-real Element of REAL
s2 . s1 is V22() V23() ext-real Element of REAL
q1 is V22() V23() ext-real Element of REAL
p2 - (s1 + 1) is V22() V23() ext-real V33() Element of REAL
max (0,(p2 - (s1 + 1))) is V22() V23() ext-real set
q1 is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
q1 + 1 is non empty V17() V21() V22() V23() ext-real positive non negative V33() finite cardinal Element of REAL
(p2 + 1) - (s1 + 1) is V22() V23() ext-real V33() Element of REAL
(len (((s2 | s1) ^ <*(u . (t + 1))*>) ^ (REAL,s1,s2))) - (s1 + 1) is V22() V23() ext-real V33() Element of REAL
dom (REAL,s1,s2) is finite V61() V62() V63() V64() V65() V66() Element of K19(NAT)
(q1 + 1) + s1 is non empty V17() V21() V22() V23() ext-real positive non negative V33() finite cardinal Element of REAL
s1 + q1 is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
(s1 + q1) + 1 is non empty V17() V21() V22() V23() ext-real positive non negative V33() finite cardinal Element of REAL
s1 + (q1 + 1) is non empty V17() V21() V22() V23() ext-real positive non negative V33() finite cardinal Element of REAL
Seg (s1 + 1) is non empty finite s1 + 1 -element V61() V62() V63() V64() V65() V66() Element of K19(NAT)
((s2 | s1) ^ <*(u . (t + 1))*>) . (s1 + 1) is V22() V23() ext-real Element of REAL
(s1 + 1) + 1 is non empty V17() V21() V22() V23() ext-real positive non negative V33() finite cardinal Element of REAL
((s1 + 1) + 1) - (s1 + 1) is V22() V23() ext-real V33() Element of REAL
(REAL,s1,s2) . (((s1 + 1) + 1) - (s1 + 1)) is V22() V23() ext-real Element of REAL
(s1 + 1) + 1 is non empty V17() V21() V22() V23() ext-real positive non negative V33() finite cardinal Element of REAL
(REAL,s1,s2) . q1 is V22() V23() ext-real Element of REAL
s2 . (s1 + q1) is V22() V23() ext-real Element of REAL
(REAL,s1,s2) . (q1 + 1) is V22() V23() ext-real Element of REAL
s2 . ((s1 + q1) + 1) is V22() V23() ext-real Element of REAL
p2 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V51() V52() V53() non-increasing FinSequence of REAL
p1 is set
Coim (m3,p1) is finite set
{p1} is non empty V12() finite 1 -element set
m3 " {p1} is finite set
card (Coim (m3,p1)) is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
Coim (s2,p1) is finite set
s2 " {p1} is finite set
card (Coim (s2,p1)) is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
q2 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V51() V52() V53() non-increasing FinSequence of REAL
Coim (q2,p1) is finite set
q2 " {p1} is finite set
card (Coim (q2,p1)) is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
((s2 | s1) ^ <*(u . (t + 1))*>) " {p1} is finite V61() V62() V63() V64() V65() V66() Element of K19(NAT)
card (((s2 | s1) ^ <*(u . (t + 1))*>) " {p1}) is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
(REAL,s1,s2) " {p1} is finite V61() V62() V63() V64() V65() V66() Element of K19(NAT)
card ((REAL,s1,s2) " {p1}) is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
(card (((s2 | s1) ^ <*(u . (t + 1))*>) " {p1})) + (card ((REAL,s1,s2) " {p1})) is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
(s2 | s1) " {p1} is finite V61() V62() V63() V64() V65() V66() Element of K19(NAT)
card ((s2 | s1) " {p1}) is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
<*(u . (t + 1))*> " {p1} is finite V61() V62() V63() V64() V65() V66() Element of K19(NAT)
card (<*(u . (t + 1))*> " {p1}) is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
(card ((s2 | s1) " {p1})) + (card (<*(u . (t + 1))*> " {p1})) is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
((card ((s2 | s1) " {p1})) + (card (<*(u . (t + 1))*> " {p1}))) + (card ((REAL,s1,s2) " {p1})) is V17() V21() V22() V23() ext-real non negative V33() finite cardinal Element of REAL
(card ((s2 | s1) " {p1})) + (card ((REAL,s1,s2) " {p1})) is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
((card ((s2 | s1) " {p1})) + (card ((REAL,s1,s2) " {p1}))) + (card (<*(u . (t + 1))*> " {p1})) is V17() V21() V22() V23() ext-real non negative V33() finite cardinal Element of REAL
(s2 | s1) ^ (REAL,s1,s2) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of REAL
((s2 | s1) ^ (REAL,s1,s2)) " {p1} is finite V61() V62() V63() V64() V65() V66() Element of K19(NAT)
card (((s2 | s1) ^ (REAL,s1,s2)) " {p1}) is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
(card (((s2 | s1) ^ (REAL,s1,s2)) " {p1})) + (card (<*(u . (t + 1))*> " {p1})) is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
m3 " {p1} is finite V61() V62() V63() V64() V65() V66() Element of K19(NAT)
card (m3 " {p1}) is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
(card (m3 " {p1})) + (card (<*(u . (t + 1))*> " {p1})) is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
m3 ^ <*(u . (t + 1))*> is Relation-like NAT -defined REAL -valued Function-like non empty finite FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of REAL
(m3 ^ <*(u . (t + 1))*>) " {p1} is finite V61() V62() V63() V64() V65() V66() Element of K19(NAT)
card ((m3 ^ <*(u . (t + 1))*>) " {p1}) is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
Coim (u,p1) is finite set
u " {p1} is finite set
card (Coim (u,p1)) is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
rng s2 is finite V61() V62() V63() Element of K19(REAL)
r2 is V22() V23() ext-real Element of REAL
rng s2 is finite V61() V62() V63() Element of K19(REAL)
r2 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V51() V52() V53() non-increasing FinSequence of REAL
s1 is V22() V23() ext-real Element of REAL
r1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V51() V52() V53() non-increasing FinSequence of REAL
t is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of REAL
len t is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
t is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
t + 1 is non empty V17() V21() V22() V23() ext-real positive non negative V33() finite cardinal Element of REAL
u is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V51() V52() V53() non-increasing FinSequence of REAL
len u is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
c₃ is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V51() V52() V53() non-increasing FinSequence of REAL
u . (t + 1) is V22() V23() ext-real Element of REAL
u | t is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of REAL
c₃ | t is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of REAL
len c₃ is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
u . (len u) is V22() V23() ext-real Element of REAL
c₃ . (len c₃) is V22() V23() ext-real Element of REAL
<*(u . (t + 1))*> is Relation-like NAT -defined REAL -valued Function-like one-to-one constant non empty V12() finite 1 -element FinSequence-like FinSubsequence-like V51() V52() V53() V55() decreasing non-decreasing non-increasing FinSequence of REAL
(u | t) ^ <*(u . (t + 1))*> is Relation-like NAT -defined REAL -valued Function-like non empty finite FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of REAL
len (u | t) is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
j is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V51() V52() V53() non-increasing FinSequence of REAL
m3 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V51() V52() V53() non-increasing FinSequence of REAL
t is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V51() V52() V53() non-increasing FinSequence of REAL
len t is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
u is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V51() V52() V53() non-increasing FinSequence of REAL
len u is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
t is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V51() V52() V53() non-increasing FinSequence of REAL
u is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V51() V52() V53() non-increasing FinSequence of REAL
len t is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
t is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of REAL
u is V22() V23() ext-real Element of REAL
u * t is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of REAL
K318(u) is Relation-like REAL -defined REAL -valued Function-like quasi_total V51() V52() V53() Element of K19(K20(REAL,REAL))
K179() is Relation-like K20(REAL,REAL) -defined REAL -valued Function-like quasi_total V51() V52() V53() Element of K19(K20(K20(REAL,REAL),REAL))
K38(REAL) is Relation-like REAL -defined REAL -valued Function-like one-to-one non empty V14( REAL ) V51() V52() V53() Element of K19(K20(REAL,REAL))
K179() [;] (u,K38(REAL)) is Relation-like Function-like set
t * K318(u) is Relation-like NAT -defined REAL -valued Function-like finite V51() V52() V53() set
c₃ is V22() V23() ext-real Element of REAL
c₃ / u is V22() V23() ext-real Element of REAL
{(c₃ / u)} is non empty V12() finite 1 -element V61() V62() V63() set
t " {(c₃ / u)} is finite V61() V62() V63() V64() V65() V66() Element of K19(NAT)
{c₃} is non empty V12() finite 1 -element V61() V62() V63() set
(u * t) " {c₃} is finite V61() V62() V63() V64() V65() V66() Element of K19(NAT)
len t is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
Seg (len t) is finite len t -element V61() V62() V63() V64() V65() V66() Element of K19(NAT)
dom t is finite V61() V62() V63() V64() V65() V66() Element of K19(NAT)
dom (u * t) is finite V61() V62() V63() V64() V65() V66() Element of K19(NAT)
len (u * t) is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
Seg (len (u * t)) is finite len (u * t) -element V61() V62() V63() V64() V65() V66() Element of K19(NAT)
n is set
j is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
t . j is V22() V23() ext-real Element of REAL
u * (t . j) is V22() V23() ext-real Element of REAL
(u * t) . j is V22() V23() ext-real Element of REAL
n is set
j is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
(u * t) . j is V22() V23() ext-real Element of REAL
t . j is V22() V23() ext-real Element of REAL
u * (t . j) is V22() V23() ext-real Element of REAL
{0} is functional non empty V12() finite V40() 1 -element V61() V62() V63() V64() V65() V66() set
t is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of REAL
0 * t is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of REAL
K318(0) is Relation-like REAL -defined REAL -valued Function-like quasi_total V51() V52() V53() Element of K19(K20(REAL,REAL))
K179() is Relation-like K20(REAL,REAL) -defined REAL -valued Function-like quasi_total V51() V52() V53() Element of K19(K20(K20(REAL,REAL),REAL))
K38(REAL) is Relation-like REAL -defined REAL -valued Function-like one-to-one non empty V14( REAL ) V51() V52() V53() Element of K19(K20(REAL,REAL))
K179() [;] (0,K38(REAL)) is Relation-like Function-like set
t * K318(0) is Relation-like NAT -defined REAL -valued Function-like finite V51() V52() V53() set
(0 * t) " {0} is finite V61() V62() V63() V64() V65() V66() Element of K19(NAT)
dom t is finite V61() V62() V63() V64() V65() V66() Element of K19(NAT)
len (0 * t) is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
Seg (len (0 * t)) is finite len (0 * t) -element V61() V62() V63() V64() V65() V66() Element of K19(NAT)
dom (0 * t) is finite V61() V62() V63() V64() V65() V66() Element of K19(NAT)
len t is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
Seg (len t) is finite len t -element V61() V62() V63() V64() V65() V66() Element of K19(NAT)
u is set
c₃ is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
(0 * t) . c₃ is V22() V23() ext-real Element of REAL
t . c₃ is V22() V23() ext-real Element of REAL
0 * (t . c₃) is V22() V23() ext-real Element of REAL
t is Relation-like Function-like set
rng t is set
u is Relation-like Function-like set
rng u is set
c₃ is set
Coim (t,c₃) is set
{c₃} is non empty V12() finite 1 -element set
t " {c₃} is set
card (Coim (t,c₃)) is V17() cardinal set
Coim (u,c₃) is set
u " {c₃} is set
card (Coim (u,c₃)) is V17() cardinal set
card (t " {c₃}) is V17() cardinal set
t is set
u is Relation-like NAT -defined t -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of t
len u is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
(t,(len u),u) is Relation-like NAT -defined t -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of t
len (t,(len u),u) is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
(len u) - (len u) is V22() V23() ext-real V33() Element of REAL
t is Relation-like Function-like set
u is Relation-like Function-like set
dom t is set
dom u is set
c₃ is set
t . c₃ is set
n is set
u . n is set
t . n is set
u . c₃ is set
id (dom t) is Relation-like dom t -defined dom t -valued Function-like one-to-one set
n .--> c₃ is Relation-like {n} -defined Function-like one-to-one finite set
{n} is non empty V12() finite 1 -element set
{n} --> c₃ is Relation-like {n} -defined {c₃} -valued Function-like constant non empty V14({n}) quasi_total finite Element of K19(K20({n},{c₃}))
{c₃} is non empty V12() finite 1 -element set
K20({n},{c₃}) is Relation-like finite set
K19(K20({n},{c₃})) is finite V40() set
c₃ .--> n is Relation-like {c₃} -defined Function-like one-to-one finite set
{c₃} --> n is Relation-like {c₃} -defined {n} -valued Function-like constant non empty V14({c₃}) quasi_total finite Element of K19(K20({c₃},{n}))
K20({c₃},{n}) is Relation-like finite set
K19(K20({c₃},{n})) is finite V40() set
(id (dom t)) +* (n .--> c₃) is Relation-like Function-like set
((id (dom t)) +* (n .--> c₃)) +* (c₃ .--> n) is Relation-like Function-like set
dom (n .--> c₃) is finite Element of K19({n})
K19({n}) is finite V40() set
dom (id (dom t)) is Element of K19((dom t))
K19((dom t)) is set
rng (id (dom t)) is Element of K19((dom t))
(id (dom t)) " is Relation-like Function-like one-to-one set
dom ((id (dom t)) ") is set
dom (c₃ .--> n) is finite Element of K19({c₃})
K19({c₃}) is finite V40() set
dom (((id (dom t)) +* (n .--> c₃)) +* (c₃ .--> n)) is set
dom ((id (dom t)) +* (n .--> c₃)) is set
(dom ((id (dom t)) +* (n .--> c₃))) \/ {c₃} is non empty set
(dom (id (dom t))) \/ {n} is non empty set
((dom (id (dom t))) \/ {n}) \/ {c₃} is non empty set
(dom t) \/ {n} is non empty set
((dom t) \/ {n}) \/ {c₃} is non empty set
(dom t) \/ {c₃} is non empty set
s1 is set
(((id (dom t)) +* (n .--> c₃)) +* (c₃ .--> n)) * (((id (dom t)) +* (n .--> c₃)) +* (c₃ .--> n)) is Relation-like Function-like set
((((id (dom t)) +* (n .--> c₃)) +* (c₃ .--> n)) * (((id (dom t)) +* (n .--> c₃)) +* (c₃ .--> n))) . s1 is set
(((id (dom t)) +* (n .--> c₃)) +* (c₃ .--> n)) . s1 is set
(((id (dom t)) +* (n .--> c₃)) +* (c₃ .--> n)) . ((((id (dom t)) +* (n .--> c₃)) +* (c₃ .--> n)) . s1) is set
(((id (dom t)) +* (n .--> c₃)) +* (c₃ .--> n)) . n is set
(((id (dom t)) +* (n .--> c₃)) +* (c₃ .--> n)) . c₃ is set
(id (dom t)) . s1 is set
(((id (dom t)) +* (n .--> c₃)) +* (c₃ .--> n)) . ((id (dom t)) . s1) is set
rng (n .--> c₃) is finite set
(rng (id (dom t))) \/ (rng (n .--> c₃)) is set
rng ((id (dom t)) +* (n .--> c₃)) is set
rng (c₃ .--> n) is finite set
(rng ((id (dom t)) +* (n .--> c₃))) \/ (rng (c₃ .--> n)) is set
(dom t) \/ (rng (c₃ .--> n)) is set
rng ((((id (dom t)) +* (n .--> c₃)) +* (c₃ .--> n)) * (((id (dom t)) +* (n .--> c₃)) +* (c₃ .--> n))) is set
rng (((id (dom t)) +* (n .--> c₃)) +* (c₃ .--> n)) is set
s1 is set
dom ((((id (dom t)) +* (n .--> c₃)) +* (c₃ .--> n)) * (((id (dom t)) +* (n .--> c₃)) +* (c₃ .--> n))) is set
(((id (dom t)) +* (n .--> c₃)) +* (c₃ .--> n)) * u is Relation-like Function-like set
dom ((((id (dom t)) +* (n .--> c₃)) +* (c₃ .--> n)) * u) is set
s1 is set
((((id (dom t)) +* (n .--> c₃)) +* (c₃ .--> n)) * u) . s1 is set
(((id (dom t)) +* (n .--> c₃)) +* (c₃ .--> n)) . s1 is set
u . ((((id (dom t)) +* (n .--> c₃)) +* (c₃ .--> n)) . s1) is set
t . s1 is set
t . s1 is set
(id (dom t)) . s1 is set
u . ((id (dom t)) . s1) is set
u . s1 is set
t . s1 is set
t . s1 is set
t . s1 is set
t is non empty set
u is Relation-like NAT -defined t -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of t
len u is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
c₃ is V17() V21() V22() V23() ext-real non negative V33() finite cardinal set
(t,c₃,u) is Relation-like NAT -defined t -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of t
len (t,c₃,u) is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
(len u) -' c₃ is V22() V23() ext-real non negative set
(len u) - c₃ is V22() V23() ext-real V33() Element of REAL
<*> t is Relation-like non-empty empty-yielding NAT -defined t -valued Function-like one-to-one constant functional empty V17() V21() V22() V23() ext-real non negative V33() finite finite-yielding V40() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V51() V52() V53() V54() V61() V62() V63() V64() V65() V66() V67() Function-yielding V73() FinSequence of t
(len u) - c₃ is V22() V23() ext-real V33() Element of REAL
u is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
dom u is finite V61() V62() V63() V64() V65() V66() Element of K19(NAT)
t is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
c₃ is set
t . c₃ is set
K20((dom u),(dom u)) is Relation-like RAT -valued INT -valued finite V51() V52() V53() V54() set
K19(K20((dom u),(dom u))) is finite V40() set
n is Relation-like dom u -defined dom u -valued Function-like quasi_total bijective finite V51() V52() V53() V54() Element of K19(K20((dom u),(dom u)))
n * u is Relation-like dom u -defined Function-like finite set
n . c₃ is V17() V21() V22() V23() ext-real non negative V33() finite cardinal Element of REAL
j is V17() V21() V22() V23() ext-real non negative V33() finite cardinal Element of REAL
u . j is set
t is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
u is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
c₃ is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
c₃ ^ t is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
c₃ ^ u is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
n is set
Coim (t,n) is finite set
{n} is non empty V12() finite 1 -element set
t " {n} is finite set
card (Coim (t,n)) is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
Coim (u,n) is finite set
u " {n} is finite set
card (Coim (u,n)) is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
Coim ((c₃ ^ t),n) is finite set
(c₃ ^ t) " {n} is finite set
card (Coim ((c₃ ^ t),n)) is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
card (u " {n}) is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
c₃ " {n} is finite set
card (c₃ " {n}) is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
(card (u " {n})) + (card (c₃ " {n})) is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
Coim ((c₃ ^ u),n) is finite set
(c₃ ^ u) " {n} is finite set
card (Coim ((c₃ ^ u),n)) is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
n is set
Coim ((c₃ ^ t),n) is finite set
{n} is non empty V12() finite 1 -element set
(c₃ ^ t) " {n} is finite set
card (Coim ((c₃ ^ t),n)) is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
Coim (t,n) is finite set
t " {n} is finite set
card (Coim (t,n)) is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
c₃ " {n} is finite set
card (c₃ " {n}) is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
(card (Coim (t,n))) + (card (c₃ " {n})) is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
(c₃ ^ u) " {n} is finite set
card ((c₃ ^ u) " {n}) is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
u " {n} is finite set
card (u " {n}) is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
(card (u " {n})) + (card (c₃ " {n})) is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
Coim ((c₃ ^ u),n) is finite set
card (Coim ((c₃ ^ u),n)) is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
Coim (u,n) is finite set
card (Coim (u,n)) is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
t is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
u is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len t is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
c₃ is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
n is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
j is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
t . j is set
(len t) - n is V22() V23() ext-real V33() Element of REAL
len u is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
m3 is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
n + m3 is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
s2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len s2 is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
r2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len r2 is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
s2 ^ r2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
s1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len s1 is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
r1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len r1 is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
s1 ^ r1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
dom r1 is finite V61() V62() V63() V64() V65() V66() Element of K19(NAT)
Seg m3 is finite m3 -element V61() V62() V63() V64() V65() V66() Element of K19(NAT)
m2 is V17() V21() V22() V23() ext-real non negative V33() finite cardinal set
n + 1 is non empty V17() V21() V22() V23() ext-real positive non negative V33() finite cardinal Element of REAL
dom r2 is finite V61() V62() V63() V64() V65() V66() Element of K19(NAT)
n + m2 is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
m2 + n is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
(len s1) + m2 is V17() V21() V22() V23() ext-real non negative V33() finite cardinal Element of REAL
r1 . m2 is set
t . ((len s1) + m2) is set
p2 is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
(len s2) + p2 is V17() V21() V22() V23() ext-real non negative V33() finite cardinal Element of REAL
u . ((len s2) + p2) is set
r2 . m2 is set
n - c₃ is V22() V23() ext-real V33() set
c₃ + 1 is non empty V17() V21() V22() V23() ext-real positive non negative V33() finite cardinal Element of REAL
m2 is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
c₃ + m2 is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
p2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len p2 is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
q2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len q2 is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
p2 ^ q2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
Seg c₃ is finite c₃ -element V61() V62() V63() V64() V65() V66() Element of K19(NAT)
dom p2 is finite V61() V62() V63() V64() V65() V66() Element of K19(NAT)
p1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len p1 is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
q1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len q1 is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
p1 ^ q1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
q1 ^ r1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
p1 ^ (q1 ^ r1) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
dom p1 is finite V61() V62() V63() V64() V65() V66() Element of K19(NAT)
q2 ^ r2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
p2 ^ (q2 ^ r2) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
x is V17() V21() V22() V23() ext-real non negative V33() finite cardinal set
p1 . x is set
t . x is set
y is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
u . y is set
p2 . x is set
j - (len p1) is V22() V23() ext-real V33() Element of REAL
x is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
n - (len p1) is V22() V23() ext-real V33() Element of REAL
Seg m2 is finite m2 -element V61() V62() V63() V64() V65() V66() Element of K19(NAT)
dom q2 is finite V61() V62() V63() V64() V65() V66() Element of K19(NAT)
1 + 0 is non empty V17() V21() V22() V23() ext-real positive non negative V33() finite cardinal Element of REAL
q1 . x is set
y is set
q2 . y is set
y is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
(len p2) + y is V17() V21() V22() V23() ext-real non negative V33() finite cardinal Element of REAL
dom s2 is finite V61() V62() V63() V64() V65() V66() Element of K19(NAT)
k is V17() V21() V22() V23() ext-real non negative V33() V34() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
u . k is set
(len p2) + 1 is non empty V17() V21() V22() V23() ext-real positive non negative V33() finite cardinal Element of REAL
m2 + (len p2) is V17() V21() V22() V23() ext-real non negative V33() finite cardinal Element of REAL
dom q1 is finite V61() V62() V63() V64() V65() V66() Element of K19(NAT)
(len p1) + x is V17() V21() V22() V23() ext-real non negative V33() finite cardinal Element of REAL
dom s1 is finite V61() V62() V63() V64() V65() V66() Element of K19(NAT)
s1 . ((len p1) + x) is set
q2 . y is set
s2 . ((len p2) + y) is set
t is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of INT
u is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V51() V52() V53() non-increasing FinSequence of REAL
rng t is finite V61() V62() V63() V64() V65() Element of K19(REAL)
rng u is finite V61() V62() V63() Element of K19(REAL)