:: deftheorem defines Sum COMSEQ_3:def 7 :
for seq being Complex_Sequence holds Sum seq = lim (Partial_Sums seq);