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> ) ) )
assume seq is summable ; :: thesis: ( Re seq is summable & Im seq is summable & Sum seq = (Sum (Re seq)) + ((Sum (Im seq)) * <i> ) )
then A1: Partial_Sums seq is convergent ;
then ( Re (Partial_Sums seq) is convergent & Im (Partial_Sums seq) is convergent ) ;
then A2: ( Partial_Sums (Re seq) is convergent & Partial_Sums (Im seq) is convergent ) by Th26;
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, Th41;
hence ( Re seq is summable & Im seq is summable & Sum seq = (Sum (Re seq)) + ((Sum (Im seq)) * <i> ) ) by A2, A3, COMPLEX1:29, SERIES_1:def 2; :: thesis: verum