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

now

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

end;

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