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