let seq be Complex_Sequence; :: thesis: ( seq is absolutely_summable implies seq is summable )
assume A1: seq is absolutely_summable ; :: thesis: seq is summable

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

let p be Real; :: thesis: ( 0 < p implies ex n being Nat st
for m being Nat st n <= m holds
|.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).| < p )
assume 0 < p ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
|.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).| < p
then consider n being Nat such that
A2: for m being Nat st n <= m holds
|.(((Partial_Sums |.seq.|) . m) - ((Partial_Sums |.seq.|) . n)).| < p by A1, SEQ_4:41;
take n = n; :: thesis: for m being Nat st n <= m holds
|.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).| < p
let m be 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: |.(((Partial_Sums |.seq.|) . m) - ((Partial_Sums |.seq.|) . n)).| < p by A2;
|.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).| <= |.(((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 Th62; :: thesis: verum