let a be FinSequence of REAL ; 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 ; ( 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))
; Sum a = s . (len a)
defpred S1[ Nat] means ( $1 <= len a implies Sum (a | $1) = s . $1 );
A3:
for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
reconsider k1 =
k as
Element of
NAT by ORDINAL1:def 12;
reconsider m =
k1 + 1 as
Nat ;
assume A4:
S1[
k]
;
S1[k + 1]
(
k + 1
<= len a implies
Sum (a | m) = s . (k + 1) )
proof
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
;
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;
verum
end;
hence
S1[
k + 1]
;
verum
end;
A13:
S1[ 0 ]
by A1, RVSUM_1:72;
for k being Nat holds S1[k]
from NAT_1:sch 2(A13, A3);
then
S1[ len a]
;
hence
Sum a = s . (len a)
by FINSEQ_1:58; verum