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

hence 0 <= Sum s by A3, SEQ_2:17; :: thesis: verum

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

Partial_Sums s is convergent
by A1;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;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

hence 0 <= Sum s by A3, SEQ_2:17; :: thesis: verum