let a be Real_Sequence; :: thesis: ( ( for n being Nat holds 0 <= a . n ) implies for n being Nat st (Partial_Sums a) . n = 0 holds
for k being Nat st k <= n holds
a . k = 0 )
assume A1: for n being Nat holds 0 <= a . n ; :: thesis: for n being Nat st (Partial_Sums a) . n = 0 holds
for k being Nat st k <= n holds
a . k = 0
let n be Nat; :: thesis: ( (Partial_Sums a) . n = 0 implies for k being Nat st k <= n holds
a . k = 0 )
assume A2: (Partial_Sums a) . n = 0 ; :: thesis: for k being Nat st k <= n holds
a . k = 0

now :: thesis: for k being Nat st k <= n holds
a . k = 0

A3: Partial_Sums a is non-decreasing by A1, SERIES_1:16;
let k be Nat; :: thesis: ( k <= n implies a . k = 0 )
assume k <= n ; :: thesis: a . k = 0
then A4: (Partial_Sums a) . k <= (Partial_Sums a) . n by A3, SEQM_3:6;
a . k <= (Partial_Sums a) . k by A1, Lm1;
hence a . k = 0 by A1, A2, A4; :: thesis: verum

end;

hence for k being Nat st k <= n holds
a . k = 0 ; :: thesis: verum