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

assume A1: for n being Nat holds 0 <= a . n ; :: thesis: for n being Nat holds 0 <= (Partial_Sums a) . n

let n be Nat; :: thesis: 0 <= (Partial_Sums a) . n

a . n <= (Partial_Sums a) . n by A1, Lm1;

hence 0 <= (Partial_Sums a) . n by A1; :: thesis: verum

assume A1: for n being Nat holds 0 <= a . n ; :: thesis: for n being Nat holds 0 <= (Partial_Sums a) . n

let n be Nat; :: thesis: 0 <= (Partial_Sums a) . n

a . n <= (Partial_Sums a) . n by A1, Lm1;

hence 0 <= (Partial_Sums a) . n by A1; :: thesis: verum