let seq be Complex_Sequence; :: thesis: ( seq is summable implies ( Re seq is summable & Im seq is summable & Sum seq = (Sum (Re seq)) + ((Sum (Im seq)) * <i>) ) )
A1: ( lim (Re (Partial_Sums seq)) = lim (Partial_Sums (Re seq)) & lim (Im (Partial_Sums seq)) = lim (Partial_Sums (Im seq)) ) by Th26;
assume A2: seq is summable ; :: thesis: ( Re seq is summable & Im seq is summable & Sum seq = (Sum (Re seq)) + ((Sum (Im seq)) * <i>) )
then Re (Partial_Sums seq) is convergent ;
then A3: Partial_Sums (Re seq) is convergent by Th26;
Im (Partial_Sums seq) is convergent by A2;
then A4: Partial_Sums (Im seq) is convergent by Th26;
( lim (Re (Partial_Sums seq)) = Re (lim (Partial_Sums seq)) & lim (Im (Partial_Sums seq)) = Im (lim (Partial_Sums seq)) ) by A2, Th41;
hence ( Re seq is summable & Im seq is summable & Sum seq = (Sum (Re seq)) + ((Sum (Im seq)) * <i>) ) by A3, A4, A1, COMPLEX1:13; :: thesis: verum