let X be ComplexUnitarySpace; :: thesis: for seq being sequence of X st seq is summable holds
Partial_Sums seq is bounded
let seq be sequence of X; :: thesis: ( seq is summable implies Partial_Sums seq is bounded )
assume seq is summable ; :: thesis: Partial_Sums seq is bounded
then Partial_Sums seq is convergent by Def2;
hence Partial_Sums seq is bounded by CLVECT_2:80; :: thesis: verum