theorem :: CLVECT_3:11
for X being ComplexUnitarySpace
for seq being sequence of X st seq is summable holds
Partial_Sums seq is bounded by CLVECT_2:80;