let n be Nat; :: thesis: for s being Real_Sequence st ( for n being Nat holds 0 <= s . n ) holds
0 <= (Partial_Sums s) . n
let s be Real_Sequence; :: thesis: ( ( for n being Nat holds 0 <= s . n ) implies 0 <= (Partial_Sums s) . n )
assume A1: for n being Nat holds 0 <= s . n ; :: thesis: 0 <= (Partial_Sums s) . n
( (Partial_Sums s) . 0 <= (Partial_Sums s) . n & 0 <= s . 0 ) by A1, SERIES_1:16, SEQM_3:11;
hence 0 <= (Partial_Sums s) . n by SERIES_1:def 1; :: thesis: verum