let n be Nat; :: thesis: for rF being real-valued XFinSequence
for S being Real_Sequence st rF = S | (n + 1) holds
Sum rF = (Partial_Sums S) . n
let rF be real-valued XFinSequence; :: thesis: for S being Real_Sequence st rF = S | (n + 1) holds
Sum rF = (Partial_Sums S) . n
let S be Real_Sequence; :: thesis: ( rF = S | (n + 1) implies Sum rF = (Partial_Sums S) . n )
A1: rF is REAL -valued by Lm7;
n + 1 c= NAT by ORDINAL1:def 2;
then A2: n + 1 c= dom S by FUNCT_2:def 1;
assume A3: rF = S | (n + 1) ; :: thesis: Sum rF = (Partial_Sums S) . n
then dom rF = (dom S) /\ (n + 1) by RELAT_1:90;
then A4: dom rF = n + 1 by A2, XBOOLE_1:28;
then consider f being Function of NAT ,REAL such that
A5: f . 0 = rF . 0 and
A6: for m being Nat st m + 1 < len rF holds
f . (m + 1) = addreal . (f . m),(rF . (m + 1)) and
A7: addreal "**" rF = f . ((len rF) - 1) by Def9, A1;
defpred S₁[ Nat] means ( $1 in dom rF implies f . $1 = (Partial_Sums S) . $1 );

A9: now

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A10: S₁[k] ; :: thesis: S₁[k + 1]
thus S₁[k + 1] :: thesis: verum

proof

assume A11: k + 1 in dom rF ; :: thesis: f . (k + 1) = (Partial_Sums S) . (k + 1)
then A12: k + 1 < len rF by NAT_1:45;
then A13: k < len rF by NAT_1:13;
A14: k in NAT by ORDINAL1:def 13;
thus f . (k + 1) = addreal . (f . k),(rF . (k + 1)) by A6, A12
.= (f . k) + (rF . (k + 1)) by BINOP_2:def 9
.= (f . k) + (S . (k + 1)) by A3, A11, FUNCT_1:70
.= (Partial_Sums S) . (k + 1) by A10, A13, NAT_1:45, SERIES_1:def 1, A14 ; :: thesis: verum

end;

end;

(Partial_Sums S) . 0 = S . 0 by SERIES_1:def 1;
then A15: S₁[ 0 ] by A3, A5, FUNCT_1:70;
for m being Nat holds S₁[m] from NAT_1:sch 2(A15, A9);
hence (Partial_Sums S) . n = f . n by A4, NAT_1:46
.= Sum rF by Th61, A7, A4 ;
:: thesis: verum