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 Th43, COMSEQ_3:53;
hence ( th rExpSeq is summable & Sum (th rExpSeq) = Re (Sum (th ExpSeq)) ) by Th43, COMPLEX1:12; :: thesis: verum