let X be ComplexBanachSpace; :: thesis: for seq being sequence of X st seq is norm_summable holds
seq is summable
let seq be sequence of X; :: thesis: ( seq is norm_summable implies seq is summable )
assume seq is norm_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 A3: n <= m ; :: thesis: ||.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).|| < p
then A4: 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 A3, Th29;
hence ||.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).|| < p by A4, XXREAL_0:2; :: thesis: verum

end;

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