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, Def8;

now

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

now

let m, n be Element of 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)).|| <= abs (((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 ( abs (((Partial_Sums ||.seq.||) . m) - ((Partial_Sums ||.seq.||) . k)) < r / 2 & abs (((Partial_Sums ||.seq.||) . n) - ((Partial_Sums ||.seq.||) . k)) < r / 2 ) by A3;
then A5: (abs (((Partial_Sums ||.seq.||) . n) - ((Partial_Sums ||.seq.||) . k))) + (abs (((Partial_Sums ||.seq.||) . m) - ((Partial_Sums ||.seq.||) . k))) < (r / 2) + (r / 2) by XREAL_1:8;
abs (((Partial_Sums ||.seq.||) . n) - ((Partial_Sums ||.seq.||) . m)) = abs ((((Partial_Sums ||.seq.||) . n) - ((Partial_Sums ||.seq.||) . k)) - (((Partial_Sums ||.seq.||) . m) - ((Partial_Sums ||.seq.||) . k))) ;
then abs (((Partial_Sums ||.seq.||) . n) - ((Partial_Sums ||.seq.||) . m)) <= (abs (((Partial_Sums ||.seq.||) . n) - ((Partial_Sums ||.seq.||) . k))) + (abs (((Partial_Sums ||.seq.||) . m) - ((Partial_Sums ||.seq.||) . k))) by COMPLEX1:57;
then abs (((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 Element of 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