let S be Real_Sequence; :: thesis: for d being XFinSequence of NAT
for n being Nat st d = S | (n + 1) holds
Sum d = (Partial_Sums S) . n
let d be XFinSequence of NAT ; :: thesis: for n being Nat st d = S | (n + 1) holds
Sum d = (Partial_Sums S) . n
let n be Nat; :: thesis: ( d = S | (n + 1) implies Sum d = (Partial_Sums S) . n )
reconsider N = n as Element of NAT by ORDINAL1:def 13;
n + 1 c= NAT by ORDINAL1:def 2;
then A1: n + 1 c= dom S by FUNCT_2:def 1;
assume A2: d = S | (n + 1) ; :: thesis: Sum d = (Partial_Sums S) . n
then dom d = (dom S) /\ (n + 1) by RELAT_1:90;
then A3: dom d = n + 1 by A1, XBOOLE_1:28;
then consider f being Function of NAT , NAT such that
A4: f . 0 = d . 0 and
A5: for m being Element of NAT st m + 1 < len d holds
f . (m + 1) = addnat . (f . m),(d . (m + 1)) and
A6: addnat "**" d = f . ((len d) - 1) by STIRL2_1:def 3;
A7: N in dom d by A3, AFINSQ_1:1;
defpred S₁[ Element of NAT ] means ( $1 in dom d implies f . $1 = (Partial_Sums S) . $1 );

A8: now

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A9: S₁[k] ; :: thesis: S₁[k + 1]
thus S₁[k + 1] :: thesis: verum

proof

assume A10: k + 1 in dom d ; :: thesis: f . (k + 1) = (Partial_Sums S) . (k + 1)
then A11: k + 1 < len d by NAT_1:45;
then A12: k < len d by NAT_1:13;
thus f . (k + 1) = addnat . (f . k),(d . (k + 1)) by A5, A11
.= (f . k) + (d . (k + 1)) by BINOP_2:def 23
.= (f . k) + (S . (k + 1)) by A2, A10, FUNCT_1:70
.= (Partial_Sums S) . (k + 1) by A9, A12, NAT_1:45, SERIES_1:def 1 ; :: thesis: verum

end;

end;

(Partial_Sums S) . 0 = S . 0 by SERIES_1:def 1;
then A13: S₁[ 0 ] by A2, A4, FUNCT_1:70;
for m being Element of NAT holds S₁[m] from NAT_1:sch 1(A13, A8);
hence Sum d = (Partial_Sums S) . n by A3, A6, A7; :: thesis: verum