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