let X be ComplexHilbertSpace; :: thesis: for seq being sequence of X st seq is absolutely_summable holds
seq is summable
let seq be sequence of X; :: thesis: ( seq is absolutely_summable implies seq is summable )
assume A1: seq is absolutely_summable ; :: thesis: seq is summable
A2: ||.seq.|| is summable by A1;

now :: thesis: for r being Real st r > 0 holds
ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
||.(((Partial_Sums seq) . n) - ((Partial_Sums seq) . m)).|| < r

let r be Real; :: thesis: ( r > 0 implies ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
||.(((Partial_Sums seq) . n) - ((Partial_Sums seq) . m)).|| < r )
assume r > 0 ; :: thesis: ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
||.(((Partial_Sums seq) . n) - ((Partial_Sums seq) . m)).|| < r
then r / 2 > 0 ;
then consider k being Nat such that
A3: for m being Nat st m >= k holds
|.(((Partial_Sums ||.seq.||) . m) - ((Partial_Sums ||.seq.||) . k)).| < r / 2 by A2, SERIES_1:21;
take k = k; :: thesis: for n, m being Nat st n >= k & m >= k holds
||.(((Partial_Sums seq) . n) - ((Partial_Sums seq) . m)).|| < r

now :: thesis: for m, n being Nat st m >= k & n >= k holds
||.(((Partial_Sums seq) . n) - ((Partial_Sums seq) . m)).|| < r

let m, n be Nat; :: thesis: ( m >= k & n >= k implies ||.(((Partial_Sums seq) . n) - ((Partial_Sums seq) . m)).|| < r )
A4: ||.(((Partial_Sums seq) . n) - ((Partial_Sums seq) . m)).|| <= |.(((Partial_Sums ||.seq.||) . n) - ((Partial_Sums ||.seq.||) . m)).| by Th39;
assume ( m >= k & n >= k ) ; :: thesis: ||.(((Partial_Sums seq) . n) - ((Partial_Sums seq) . m)).|| < r
then ( |.(((Partial_Sums ||.seq.||) . m) - ((Partial_Sums ||.seq.||) . k)).| < r / 2 & |.(((Partial_Sums ||.seq.||) . n) - ((Partial_Sums ||.seq.||) . k)).| < r / 2 ) by A3;
then A5: |.(((Partial_Sums ||.seq.||) . n) - ((Partial_Sums ||.seq.||) . k)).| + |.(((Partial_Sums ||.seq.||) . m) - ((Partial_Sums ||.seq.||) . k)).| < (r / 2) + (r / 2) by XREAL_1:8;
|.(((Partial_Sums ||.seq.||) . n) - ((Partial_Sums ||.seq.||) . m)).| = |.((((Partial_Sums ||.seq.||) . n) - ((Partial_Sums ||.seq.||) . k)) - (((Partial_Sums ||.seq.||) . m) - ((Partial_Sums ||.seq.||) . k))).| ;
then |.(((Partial_Sums ||.seq.||) . n) - ((Partial_Sums ||.seq.||) . m)).| <= |.(((Partial_Sums ||.seq.||) . n) - ((Partial_Sums ||.seq.||) . k)).| + |.(((Partial_Sums ||.seq.||) . m) - ((Partial_Sums ||.seq.||) . k)).| by COMPLEX1:57;
then |.(((Partial_Sums ||.seq.||) . n) - ((Partial_Sums ||.seq.||) . m)).| < r by A5, XXREAL_0:2;
hence ||.(((Partial_Sums seq) . n) - ((Partial_Sums seq) . m)).|| < r by A4, XXREAL_0:2; :: thesis: verum

end;

hence for n, m being Nat st n >= k & m >= k holds
||.(((Partial_Sums seq) . n) - ((Partial_Sums seq) . m)).|| < r ; :: thesis: verum

end;

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