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

a . k = 0 ; :: thesis: verum

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

hence
for k being Nat st k <= n holds a . k = 0

A3:
Partial_Sums a is V48()
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;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

a . k = 0 ; :: thesis: verum