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 Lm3;
n + 1 c= NAT ;
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:61;
then A4: dom rF = n + 1 by A2, XBOOLE_1:28;
then consider f being sequence of 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 Def8, A1;
defpred S1[ Nat] means ( $1 in dom rF implies f . $1 = (Partial_Sums S) . $1 );
A8: now :: thesis: for k being Nat st S1[k] holds
S1[k + 1]
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A9: S1[k] ; :: thesis: S1[k + 1]
thus S1[k + 1] :: thesis: verum
proof
assume A10: k + 1 in dom rF ; :: thesis: f . (k + 1) = (Partial_Sums S) . (k + 1)
then A11: k + 1 < len rF by AFINSQ_1:86;
then A12: k < len rF by NAT_1:13;
thus f . (k + 1) = addreal . ((f . k),(rF . (k + 1))) by A6, A11
.= (f . k) + (rF . (k + 1)) by BINOP_2:def 9
.= (f . k) + (S . (k + 1)) by A3, A10, FUNCT_1:47
.= (Partial_Sums S) . (k + 1) by A9, A12, AFINSQ_1:86, SERIES_1:def 1 ; :: thesis: verum
end;
end;
(Partial_Sums S) . 0 = S . 0 by SERIES_1:def 1;
then A13: S1[ 0 ] by A3, A5, FUNCT_1:47;
A14: n in Segm (n + 1) by NAT_1:45;
for m being Nat holds S1[m] from NAT_1:sch 2(A13, A8);
 hence (Partial_Sums S) . n = f . n by A4, A14
.= Sum rF by Th47, A7, A4 ;
:: thesis: verum