:: deftheorem Def9 defines absolutely_summable COMSEQ_3:def 9 :
for seq being Complex_Sequence holds
( seq is absolutely_summable iff |.seq.| is summable );