:: deftheorem Def1 defines summable CLVECT_3:def 1 :
for X being ComplexUnitarySpace
for seq being sequence of X holds
( seq is summable iff Partial_Sums seq is convergent );