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