:: 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