let th be Real; :: thesis: exp_R . th = Re (Sum (th ExpSeq))
exp_R . th = Sum (th rExpSeq) by Def22;
hence exp_R . th = Re (Sum (th ExpSeq)) by Th44; :: thesis: verum