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