let a be non empty FinSequence of REAL ; :: thesis: for f being FinSequence of NAT

for k being Nat

for R1 being real-valued FinSequence st dom f = dom a & rng f = Seg k & len R1 = k & ( for j being Nat st j in dom R1 holds

R1 . j = SumBin (a,f,{j}) ) holds

Sum R1 = SumBin (a,f,(rng f))

let f be FinSequence of NAT ; :: thesis: for k being Nat

for R1 being real-valued FinSequence st dom f = dom a & rng f = Seg k & len R1 = k & ( for j being Nat st j in dom R1 holds

R1 . j = SumBin (a,f,{j}) ) holds

Sum R1 = SumBin (a,f,(rng f))

let k be Nat; :: thesis: for R1 being real-valued FinSequence st dom f = dom a & rng f = Seg k & len R1 = k & ( for j being Nat st j in dom R1 holds

R1 . j = SumBin (a,f,{j}) ) holds

Sum R1 = SumBin (a,f,(rng f))

let R1 be real-valued FinSequence; :: thesis: ( dom f = dom a & rng f = Seg k & len R1 = k & ( for j being Nat st j in dom R1 holds

R1 . j = SumBin (a,f,{j}) ) implies Sum R1 = SumBin (a,f,(rng f)) )

assume that

L00: dom f = dom a and

L30: rng f = Seg k and

L40: len R1 = k and

L41: for j being Nat st j in dom R1 holds

R1 . j = SumBin (a,f,{j}) ; :: thesis: Sum R1 = SumBin (a,f,(rng f))

A00: dom R1 = Seg k by L40, FINSEQ_1:def 3;

rng f <> {} by L00, RELAT_1:42;

then 0 < k by L30;

then A94: 0 + 1 <= k by INT_1:7;

defpred S_{1}[ Nat] means for r1segi being real-valued FinSequence st r1segi = R1 | (Seg $1) holds

Sum r1segi = SumBin (a,f,(Seg $1));

reconsider k = k as Element of NAT by ORDINAL1:def 12;

for r1segi being real-valued FinSequence st r1segi = R1 | (Seg 1) holds

Sum r1segi = SumBin (a,f,(Seg 1))_{1}[1]
;

A60: for i being Element of NAT st 1 <= i & i < k & S_{1}[i] holds

S_{1}[i + 1]

S_{1}[i]
from INT_1:sch 7(A30, A60);

R1 = R1 | (dom R1)

.= R1 | (Seg k) by L40, FINSEQ_1:def 3 ;

hence Sum R1 = SumBin (a,f,(rng f)) by L30, A94, A89; :: thesis: verum

for k being Nat

for R1 being real-valued FinSequence st dom f = dom a & rng f = Seg k & len R1 = k & ( for j being Nat st j in dom R1 holds

R1 . j = SumBin (a,f,{j}) ) holds

Sum R1 = SumBin (a,f,(rng f))

let f be FinSequence of NAT ; :: thesis: for k being Nat

for R1 being real-valued FinSequence st dom f = dom a & rng f = Seg k & len R1 = k & ( for j being Nat st j in dom R1 holds

R1 . j = SumBin (a,f,{j}) ) holds

Sum R1 = SumBin (a,f,(rng f))

let k be Nat; :: thesis: for R1 being real-valued FinSequence st dom f = dom a & rng f = Seg k & len R1 = k & ( for j being Nat st j in dom R1 holds

R1 . j = SumBin (a,f,{j}) ) holds

Sum R1 = SumBin (a,f,(rng f))

let R1 be real-valued FinSequence; :: thesis: ( dom f = dom a & rng f = Seg k & len R1 = k & ( for j being Nat st j in dom R1 holds

R1 . j = SumBin (a,f,{j}) ) implies Sum R1 = SumBin (a,f,(rng f)) )

assume that

L00: dom f = dom a and

L30: rng f = Seg k and

L40: len R1 = k and

L41: for j being Nat st j in dom R1 holds

R1 . j = SumBin (a,f,{j}) ; :: thesis: Sum R1 = SumBin (a,f,(rng f))

A00: dom R1 = Seg k by L40, FINSEQ_1:def 3;

rng f <> {} by L00, RELAT_1:42;

then 0 < k by L30;

then A94: 0 + 1 <= k by INT_1:7;

defpred S

Sum r1segi = SumBin (a,f,(Seg $1));

reconsider k = k as Element of NAT by ORDINAL1:def 12;

for r1segi being real-valued FinSequence st r1segi = R1 | (Seg 1) holds

Sum r1segi = SumBin (a,f,(Seg 1))

proof

then A30:
S
let r1seg1 be real-valued FinSequence; :: thesis: ( r1seg1 = R1 | (Seg 1) implies Sum r1seg1 = SumBin (a,f,(Seg 1)) )

assume A10: r1seg1 = R1 | (Seg 1) ; :: thesis: Sum r1seg1 = SumBin (a,f,(Seg 1))

then A18: dom r1seg1 = Seg 1 by A94, L40, FINSEQ_1:17;

A19: 1 in dom R1 by A00, A94;

1 in Seg 1 ;

then A20: r1seg1 . 1 = R1 . 1 by A10, FUNCT_1:49

.= SumBin (a,f,(Seg 1)) by A19, L41, FINSEQ_1:2 ;

r1seg1 = <*(SumBin (a,f,(Seg 1)))*> by A18, A20, FINSEQ_1:def 8;

hence Sum r1seg1 = SumBin (a,f,(Seg 1)) by RVSUM_1:73; :: thesis: verum

end;assume A10: r1seg1 = R1 | (Seg 1) ; :: thesis: Sum r1seg1 = SumBin (a,f,(Seg 1))

then A18: dom r1seg1 = Seg 1 by A94, L40, FINSEQ_1:17;

A19: 1 in dom R1 by A00, A94;

1 in Seg 1 ;

then A20: r1seg1 . 1 = R1 . 1 by A10, FUNCT_1:49

.= SumBin (a,f,(Seg 1)) by A19, L41, FINSEQ_1:2 ;

r1seg1 = <*(SumBin (a,f,(Seg 1)))*> by A18, A20, FINSEQ_1:def 8;

hence Sum r1seg1 = SumBin (a,f,(Seg 1)) by RVSUM_1:73; :: thesis: verum

A60: for i being Element of NAT st 1 <= i & i < k & S

S

proof

A89:
for i being Element of NAT st 1 <= i & i <= k holds
let i0 be Element of NAT ; :: thesis: ( 1 <= i0 & i0 < k & S_{1}[i0] implies S_{1}[i0 + 1] )

assume that

1 <= i0 and

A62: i0 < k and

A63: S_{1}[i0]
; :: thesis: S_{1}[i0 + 1]

reconsider r1segi0 = R1 | (Seg i0) as real-valued FinSequence by FINSEQ_1:15;

reconsider r1segi0p = R1 | (Seg (i0 + 1)) as real-valued FinSequence by FINSEQ_1:15;

A733: 1 <= i0 + 1 by NAT_1:12;

i0 + 1 <= k by A62, INT_1:7;

then A74: i0 + 1 in dom R1 by A733, A00;

then A80: Sum r1segi0p = Sum (r1segi0 ^ <*(R1 . (i0 + 1))*>) by FINSEQ_5:10

.= (Sum r1segi0) + (R1 . (i0 + 1)) by RVSUM_1:74

.= (Sum r1segi0) + (SumBin (a,f,{(i0 + 1)})) by A74, L41 ;

SumBin (a,f,(Seg (i0 + 1))) = SumBin (a,f,((Seg i0) \/ {(i0 + 1)})) by FINSEQ_1:9

.= (SumBin (a,f,(Seg i0))) + (SumBin (a,f,{(i0 + 1)})) by FINSEQ_3:14, NF270

.= Sum r1segi0p by A63, A80 ;

hence for r1segi being real-valued FinSequence st r1segi = R1 | (Seg (i0 + 1)) holds

Sum r1segi = SumBin (a,f,(Seg (i0 + 1))) ; :: thesis: verum

end;assume that

1 <= i0 and

A62: i0 < k and

A63: S

reconsider r1segi0 = R1 | (Seg i0) as real-valued FinSequence by FINSEQ_1:15;

reconsider r1segi0p = R1 | (Seg (i0 + 1)) as real-valued FinSequence by FINSEQ_1:15;

A733: 1 <= i0 + 1 by NAT_1:12;

i0 + 1 <= k by A62, INT_1:7;

then A74: i0 + 1 in dom R1 by A733, A00;

then A80: Sum r1segi0p = Sum (r1segi0 ^ <*(R1 . (i0 + 1))*>) by FINSEQ_5:10

.= (Sum r1segi0) + (R1 . (i0 + 1)) by RVSUM_1:74

.= (Sum r1segi0) + (SumBin (a,f,{(i0 + 1)})) by A74, L41 ;

SumBin (a,f,(Seg (i0 + 1))) = SumBin (a,f,((Seg i0) \/ {(i0 + 1)})) by FINSEQ_1:9

.= (SumBin (a,f,(Seg i0))) + (SumBin (a,f,{(i0 + 1)})) by FINSEQ_3:14, NF270

.= Sum r1segi0p by A63, A80 ;

hence for r1segi being real-valued FinSequence st r1segi = R1 | (Seg (i0 + 1)) holds

Sum r1segi = SumBin (a,f,(Seg (i0 + 1))) ; :: thesis: verum

S

R1 = R1 | (dom R1)

.= R1 | (Seg k) by L40, FINSEQ_1:def 3 ;

hence Sum R1 = SumBin (a,f,(rng f)) by L30, A94, A89; :: thesis: verum