theorem Th57: :: COMSEQ_3:57

for seq being Complex_Sequence st Re seq is summable & Im seq is summable holds
( seq is summable & Sum seq = (Sum (Re seq)) + ((Sum (Im seq)) * <i>) )