let seq be Complex_Sequence; :: thesis: ( seq is absolutely_summable implies seq is summable )
assume seq is absolutely_summable ; :: thesis: seq is summable
then |.seq.| is summable ;
then A1: Partial_Sums |.seq.| is convergent by SERIES_1:def 2;

now

let p be Real; :: thesis: ( 0 < p implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).| < p )
assume 0 < p ; :: thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).| < p
then consider n being Element of NAT such that
A2: for m being Element of NAT st n <= m holds
abs (((Partial_Sums |.seq.|) . m) - ((Partial_Sums |.seq.|) . n)) < p by A1, SEQ_4:58;
take n = n; :: thesis: for m being Element of NAT st n <= m holds
|.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).| < p
let m be Element of NAT ; :: thesis: ( n <= m implies |.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).| < p )
assume n <= m ; :: thesis: |.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).| < p
then A3: abs (((Partial_Sums |.seq.|) . m) - ((Partial_Sums |.seq.|) . n)) < p by A2;
|.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).| <= abs (((Partial_Sums |.seq.|) . m) - ((Partial_Sums |.seq.|) . n)) by Th31;
hence |.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).| < p by A3, XXREAL_0:2; :: thesis: verum

end;

hence seq is summable by Th63; :: thesis: verum