let s be Real_Sequence; :: thesis: ( s is absolutely_summable implies s is summable )
assume s is absolutely_summable ; :: thesis: s is summable
then A1: abs s is summable ;

now :: thesis: for r being Real st 0 < r holds
ex n being Nat st
for m being Nat st n <= m holds
|.(((Partial_Sums s) . m) - ((Partial_Sums s) . n)).| < r

let r be Real; :: thesis: ( 0 < r implies ex n being Nat st
for m being Nat st n <= m holds
|.(((Partial_Sums s) . m) - ((Partial_Sums s) . n)).| < r )
assume 0 < r ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
|.(((Partial_Sums s) . m) - ((Partial_Sums s) . n)).| < r
then consider n being Nat such that
A2: for m being Nat st n <= m holds
|.(((Partial_Sums (abs s)) . m) - ((Partial_Sums (abs s)) . n)).| < r by A1, Th21;
take n = n; :: thesis: for m being Nat st n <= m holds
|.(((Partial_Sums s) . m) - ((Partial_Sums s) . n)).| < r
let m be Nat; :: thesis: ( n <= m implies |.(((Partial_Sums s) . m) - ((Partial_Sums s) . n)).| < r )
assume A3: n <= m ; :: thesis: |.(((Partial_Sums s) . m) - ((Partial_Sums s) . n)).| < r
then A4: |.(((Partial_Sums s) . m) - ((Partial_Sums s) . n)).| <= |.(((Partial_Sums (abs s)) . m) - ((Partial_Sums (abs s)) . n)).| by Th34;
|.(((Partial_Sums (abs s)) . m) - ((Partial_Sums (abs s)) . n)).| < r by A2, A3;
hence |.(((Partial_Sums s) . m) - ((Partial_Sums s) . n)).| < r by A4, XXREAL_0:2; :: thesis: verum

end;

hence s is summable by Th21; :: thesis: verum