let s be Real_Sequence; :: thesis:
let n be Nat; :: thesis:
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]

let k be Nat; :: thesis:
assume A4: S₁[k] ; :: thesis:
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:

end;