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