:: deftheorem Def8 defines summable COMSEQ_3:def 8 :
for seq being Complex_Sequence holds
( seq is summable iff Partial_Sums seq is convergent );