let s be Real_Sequence; :: thesis: ( ( for n being Element of NAT holds 0 <= s . n ) & s is summable implies s is absolutely_summable )
assume that
A1: for n being Element of NAT holds 0 <= s . n and
A2: s is summable ; :: thesis: s is absolutely_summable
A3: Partial_Sums s is convergent by A2, Def2;

now

let n be Element of NAT ; :: thesis: s . n = abs (s . n)
0 <= s . n by A1;
hence s . n = abs (s . n) by ABSVALUE:def 1; :: thesis: verum

end;

then Partial_Sums (abs s) is convergent by A3, SEQ_1:16;
then abs s is summable by Def2;
hence s is absolutely_summable by Def5; :: thesis: verum