let th be Real; :: thesis: ( th rExpSeq is summable & Sum (th rExpSeq ) = Re (Sum (th ExpSeq )) )
( Sum (th ExpSeq ) = (Sum (Re (th ExpSeq ))) + ((Sum (Im (th ExpSeq ))) * <i> ) & Sum (th rExpSeq ) = Sum (Re (th ExpSeq )) ) by Th48, COMSEQ_3:54;
hence ( th rExpSeq is summable & Sum (th rExpSeq ) = Re (Sum (th ExpSeq )) ) by Th48, COMPLEX1:28; :: thesis: verum