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