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