let s be Real_Sequence; :: thesis: ( s is summable & ( for n being Nat holds 0 <= s . n ) implies 0 <= Sum s )
assume that
A1: s is summable and
A2: for n being Nat holds 0 <= s . n ; :: thesis: 0 <= Sum s
A3: now :: thesis: for n being Nat holds 0 <= (Partial_Sums s) . n
let n be Nat; :: thesis: 0 <= (Partial_Sums s) . n
A4: (Partial_Sums s) . 0 = s . 0 by Def1;
( (Partial_Sums s) . 0 <= (Partial_Sums s) . n & 0 <= s . 0 ) by A2, Th16, SEQM_3:11;
hence 0 <= (Partial_Sums s) . n by A4; :: thesis: verum
end;
Partial_Sums s is convergent by A1;
hence 0 <= Sum s by A3, SEQ_2:17; :: thesis: verum