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

t ^ c

u ^ c

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

(t ^ c

card (Coim ((t ^ c

Coim (c

c

card (Coim (c

(card (Coim (u,n))) + (card (Coim (c

Coim ((u ^ c

(u ^ c

card (Coim ((u ^ c

n is set

Coim ((t ^ c

{n} is non empty V12() finite 1 -element set

(t ^ c

card (Coim ((t ^ c

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

c

card (Coim (c

(card (Coim (t,n))) + (card (Coim (c

Coim ((u ^ c

(u ^ c

card (Coim ((u ^ c

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

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

Coim ((t ^ u),c

{c

(t ^ u) " {c

card (Coim ((t ^ u),c

Coim ((u ^ t),c

(u ^ t) " {c

card (Coim ((u ^ t),c

card (Coim ((t ^ u),c

u " {c

card (u " {c

t " {c

card (t " {c

(card (u " {c

card (Coim ((u ^ t),c

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

c

rng c

dom c

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

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

c

card (Coim (c

card (Coim (c

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

c

dom (c

card (dom (c

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

dom (c

dom c

(dom c

(dom c

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

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

<*(c

r2 ^ <*(c

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

c

(c

((c

c

(u \ { the Element of n}) /\ (c

((u \ { the Element of n}) /\ (c

{ the Element of n} /\ (c

((u \ { the Element of n}) /\ (c

(u \ { the Element of n}) \/ { the Element of n} is non empty finite set

((u \ { the Element of n}) \/ { the Element of n}) /\ (c

u \/ { the Element of n} is non empty finite set

(u \/ { the Element of n}) /\ (c

u /\ (c

(c

<*(c

Coim ((c

card (Coim ((c

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

dom <*(c

p2 is set

(c

card ((c

p2 is set

<*(c

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

<*(c

the Element of (c

(c

card ((c

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

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

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}) /\ (c

((u \ { the Element of n}) /\ (c

(c

((c

(((c

(u \ { the Element of n}) /\ { the Element of n} is finite Element of K19(u)

(c

((c

{} /\ (c

Coim ((c

card (Coim ((c

card ((c

(card ((c

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

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

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

len c

dom c

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

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

(u,c

len c

(len c

len (u,c

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

rng c

K19(t) is set

m3 is set

dom (u,c

s2 is V17() V21() V22() V23() ext-real non negative V33() finite cardinal set

(u,c

s2 + u is V17() V21() V22() V23() ext-real non negative V33() finite cardinal set

dom c

c

len c

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

t is V17() V21() V22() V23() ext-real non negative V33() finite cardinal set

u is non empty set

c

len c

c

dom c

Seg (len c

Seg t is finite t -element V61() V62() V63() V64() V65() V66() Element of K19(NAT)

c

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

n is V17() V21() V22() V23() ext-real non negative V33() finite cardinal set

Seg c

u | c

(u | c

u . n is set

u | (Seg c

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

dom (u | c

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

c

u . (c

u | c

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

len (u | c

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

Seg (len (u | c

dom (u | c

((u | c

(u | c

u . m3 is set

u . m3 is set

((u | c

u . m3 is set

((u | c

len ((u | c

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

t is non empty set

u is Relation-like NAT -defined t -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of t

c

u | c

(t,c

(u | c

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

len (t,c

(len u) - c

len ((u | c

c

dom (u | c

Seg c

j is V17() V21() V22() V23() ext-real non negative V33() finite cardinal set

((u | c

(u | c

u . j is set

j - c

max (0,(j - c

c

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

(t,c

m3 + c

u . (m3 + c

u . j is set

((u | c

u . j is set

((u | c

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

c

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

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

((j | s2) | r1) ^ <*(n . (c

n | c

(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

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

card ((n | c

<*(n . (c

card (<*(n . (c

(card ((n | c

(j | r1) ^ <*(n . (c

((j | r1) ^ <*(n . (c

(((j | r1) ^ <*(n . (c

card ((((j | r1) ^ <*(n . (c

((j | r1) ^ <*(n . (c

card (((j | r1) ^ <*(n . (c

(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

(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

((card ((j | r1) " {p2})) + (card (<*(n . (c

(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

(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

Coim ((n | c

(n | c

card (Coim ((n | c

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

Sum (n | c

K240(REAL,(n | c

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

K240(REAL,<*(n . (c

(Sum ((j | r1) ^ (REAL,s2,j))) + (Sum <*(n . (c

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

(Sum (j | r1)) + (Sum <*(n . (c

((Sum (j | r1)) + (Sum <*(n . (c

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

n is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V51() V52() V53() FinSequence of REAL

len c

Sum c

K240(REAL,c

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

u . c

t . c

c

t . (c

(t . c

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

len c

c

(len c

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

u . n is V22() V23() ext-real Element of REAL

c

u . n is V22() V23() ext-real Element 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 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

c

c

t . (c

t | (c

((t | (c

(t) | c

((t) | c

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

c

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

len (t | (c

len ((t | (c

dom ((t | (c

Seg (c

(t | (c

((t | (c

len ((t) | c

Seg (len ((t) | c

dom ((t) | c

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

(((t) | c

Seg c

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

(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

(t | (c

(len ((t | (c

(t | (c

((t | (c

((t | (c

(((t) | c

((t | (c

(((t) | c

len (((t) | c

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