let a be FinSequence of REAL ; :: thesis: for s being XFinSequence of REAL st s . 0 = 0 & ( for i being Nat st i < len a holds

s . (i + 1) = (s . i) + (a . (i + 1)) ) holds

Sum a = s . (len a)

let s be XFinSequence of REAL ; :: thesis: ( s . 0 = 0 & ( for i being Nat st i < len a holds

s . (i + 1) = (s . i) + (a . (i + 1)) ) implies Sum a = s . (len a) )

assume that

A1: s . 0 = 0 and

A2: for i being Nat st i < len a holds

s . (i + 1) = (s . i) + (a . (i + 1)) ; :: thesis: Sum a = s . (len a)

defpred S_{1}[ Nat] means ( $1 <= len a implies Sum (a | $1) = s . $1 );

A3: for k being Nat st S_{1}[k] holds

S_{1}[k + 1]
_{1}[ 0 ]
by A1, RVSUM_1:72;

for k being Nat holds S_{1}[k]
from NAT_1:sch 2(A13, A3);

then S_{1}[ len a]
;

hence Sum a = s . (len a) by FINSEQ_1:58; :: thesis: verum

s . (i + 1) = (s . i) + (a . (i + 1)) ) holds

Sum a = s . (len a)

let s be XFinSequence of REAL ; :: thesis: ( s . 0 = 0 & ( for i being Nat st i < len a holds

s . (i + 1) = (s . i) + (a . (i + 1)) ) implies Sum a = s . (len a) )

assume that

A1: s . 0 = 0 and

A2: for i being Nat st i < len a holds

s . (i + 1) = (s . i) + (a . (i + 1)) ; :: thesis: Sum a = s . (len a)

defpred S

A3: for k being Nat st S

S

proof

A13:
S
let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

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

reconsider m = k1 + 1 as Nat ;

assume A4: S_{1}[k]
; :: thesis: S_{1}[k + 1]

( k + 1 <= len a implies Sum (a | m) = s . (k + 1) )_{1}[k + 1]
; :: thesis: verum

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

reconsider m = k1 + 1 as Nat ;

assume A4: S

( k + 1 <= len a implies Sum (a | m) = s . (k + 1) )

proof

hence
S
reconsider x0 = <*(a /. m)*> as FinSequence of REAL ;

reconsider rx = a /. m as Element of REAL ;

reconsider q0 = a | k as FinSequence of REAL ;

assume A5: k + 1 <= len a ; :: thesis: Sum (a | m) = s . (k + 1)

then A6: a | m = (a | k) ^ <*(a /. m)*> by FINSEQ_5:82;

A7: 1 <= k + 1 by NAT_1:11;

then m in Seg (len a) by A5, FINSEQ_1:1;

then A8: m in dom a by FINSEQ_1:def 3;

m in Seg m by A7, FINSEQ_1:1;

then m in Seg (len (a | m)) by A5, FINSEQ_1:59;

then A9: m in dom (a | m) by FINSEQ_1:def 3;

Sum x0 = rx by RVSUM_1:73;

then A10: Sum (a | m) = (s . k) + rx by A4, A5, A6, NAT_1:13, RVSUM_1:75;

A11: len (a | m) = m by A5, FINSEQ_1:59;

A12: k < len a by A5, NAT_1:13;

len (a | m) = (len q0) + (len <*rx*>) by A6, FINSEQ_1:22

.= (len q0) + 1 by FINSEQ_1:40 ;

then rx = (a | m) . m by A6, A11, FINSEQ_1:42

.= (a | m) /. m by A9, PARTFUN1:def 6

.= a /. m by A9, FINSEQ_4:70

.= a . m by A8, PARTFUN1:def 6 ;

hence Sum (a | m) = s . (k + 1) by A2, A12, A10; :: thesis: verum

end;reconsider rx = a /. m as Element of REAL ;

reconsider q0 = a | k as FinSequence of REAL ;

assume A5: k + 1 <= len a ; :: thesis: Sum (a | m) = s . (k + 1)

then A6: a | m = (a | k) ^ <*(a /. m)*> by FINSEQ_5:82;

A7: 1 <= k + 1 by NAT_1:11;

then m in Seg (len a) by A5, FINSEQ_1:1;

then A8: m in dom a by FINSEQ_1:def 3;

m in Seg m by A7, FINSEQ_1:1;

then m in Seg (len (a | m)) by A5, FINSEQ_1:59;

then A9: m in dom (a | m) by FINSEQ_1:def 3;

Sum x0 = rx by RVSUM_1:73;

then A10: Sum (a | m) = (s . k) + rx by A4, A5, A6, NAT_1:13, RVSUM_1:75;

A11: len (a | m) = m by A5, FINSEQ_1:59;

A12: k < len a by A5, NAT_1:13;

len (a | m) = (len q0) + (len <*rx*>) by A6, FINSEQ_1:22

.= (len q0) + 1 by FINSEQ_1:40 ;

then rx = (a | m) . m by A6, A11, FINSEQ_1:42

.= (a | m) /. m by A9, PARTFUN1:def 6

.= a /. m by A9, FINSEQ_4:70

.= a . m by A8, PARTFUN1:def 6 ;

hence Sum (a | m) = s . (k + 1) by A2, A12, A10; :: thesis: verum

for k being Nat holds S

then S

hence Sum a = s . (len a) by FINSEQ_1:58; :: thesis: verum