let X be RealBanachSpace; :: 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 A1: Partial_Sums ||.seq.|| is convergent by SERIES_1:def 2;

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;
reconsider n = n as Nat ;
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 A3: n <= m ; :: thesis: ||.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).|| < p
then A4: ||.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).|| <= |.(((Partial_Sums ||.seq.||) . m) - ((Partial_Sums ||.seq.||) . n)).| by Th25;
|.(((Partial_Sums ||.seq.||) . m) - ((Partial_Sums ||.seq.||) . n)).| < p by A2, A3;
hence ||.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).|| < p by A4, XXREAL_0:2; :: thesis: verum

end;

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