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

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