let s be Real_Sequence; :: thesis: ( ( for n being Nat holds 0 <= s . n ) & s is summable implies s is absolutely_summable )
assume that
A1: for n being Nat holds 0 <= s . n and
A2: s is summable ; :: thesis: s is absolutely_summable
A3: for n being Nat holds s . n = |.(s . n).| by A1, ABSVALUE:def 1;
Partial_Sums s is convergent by A2;
then Partial_Sums (abs s) is convergent by A3, SEQ_1:12;
then abs s is summable ;
hence s is absolutely_summable ; :: thesis: verum