let f be Real_Sequence; :: thesis:
given n being Nat such that A1: for k being Nat st k >= n holds
f . k = 0 ; :: thesis:
set p = Partial_Sums f;
reconsider pk = (Partial_Sums f) . n as Real ;
set r = seq_const pk;
for k being Nat st k >= n holds
(Partial_Sums f) . k = (seq_const pk) . k

let k be Nat; :: thesis:
assume A2: k >= n ; :: thesis:
defpred S₁[ Nat] means (Partial_Sums f) . $1 = (seq_const pk) . $1;
A3: S₁[n] by SEQ_1:57;
A4: for i being Nat st n <= i & S₁[i] holds
S₁[i + 1]

let i be Nat; :: thesis:
assume A5: n <= i ; :: thesis:
assume A6: S₁[i] ; :: thesis:
(Partial_Sums f) . (i + 1) = ((Partial_Sums f) . i) + (f . (i + 1)) by SERIES_1:def 1
.= ((seq_const pk) . i) + 0 by A1, A5, A6, NAT_1:12
.= pk by SEQ_1:57
.= (seq_const pk) . (i + 1) ;
hence S₁[i + 1] ; :: thesis:

end;

end;