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