let s be Real_Sequence; :: thesis: for n being Nat holds (Partial_Sums s) . n = Sum (Shift ((s | (Segm (n + 1))),1))
let n be Nat; :: thesis: (Partial_Sums s) . n = Sum (Shift ((s | (Segm (n + 1))),1))
defpred S₁[ Nat] means (Partial_Sums s) . $1 = Sum (Shift ((s | (Segm ($1 + 1))),1));
A1: (Partial_Sums s) . 0 = s . 0 by SERIES_1:def 1;
Shift ((s | (Segm (0 + 1))),1) = <*(s . 0)*> by SH4;
then A2: S₁[ 0 ] by A1, RVSUM_1:73;
A3: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A4: S₁[k] ; :: thesis: S₁[k + 1]
A5: (Partial_Sums s) . (k + 1) = ((Partial_Sums s) . k) + (s . (k + 1)) by SERIES_1:def 1;
Shift ((s | (Segm ((k + 1) + 1))),1) = (Shift ((s | (Segm (k + 1))),1)) ^ <*(s . (k + 1))*> by SH4;
hence S₁[k + 1] by A4, A5, RVSUM_1:74; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A2, A3);
hence (Partial_Sums s) . n = Sum (Shift ((s | (Segm (n + 1))),1)) ; :: thesis: verum