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 by Def5;

now

let r be real number ; :: thesis: ( 0 < r implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs (((Partial_Sums s) . m) - ((Partial_Sums s) . n)) < r )
assume 0 < r ; :: thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs (((Partial_Sums s) . m) - ((Partial_Sums s) . n)) < r
then consider n being Element of NAT such that
A2: for m being Element of NAT st n <= m holds
abs (((Partial_Sums (abs s)) . m) - ((Partial_Sums (abs s)) . n)) < r by A1, Th25;
take n = n; :: thesis: for m being Element of NAT st n <= m holds
abs (((Partial_Sums s) . m) - ((Partial_Sums s) . n)) < r
let m be Element of NAT ; :: thesis: ( n <= m implies abs (((Partial_Sums s) . m) - ((Partial_Sums s) . n)) < r )
assume A3: n <= m ; :: thesis: abs (((Partial_Sums s) . m) - ((Partial_Sums s) . n)) < r
then A4: abs (((Partial_Sums s) . m) - ((Partial_Sums s) . n)) <= abs (((Partial_Sums (abs s)) . m) - ((Partial_Sums (abs s)) . n)) by Th39;
abs (((Partial_Sums (abs s)) . m) - ((Partial_Sums (abs s)) . n)) < r by A2, A3;
hence abs (((Partial_Sums s) . m) - ((Partial_Sums s) . n)) < r by A4, XXREAL_0:2; :: thesis: verum

end;

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