let th be Real; :: thesis: exp th = exp_R th
thus exp th = Sum (th ExpSeq) by Def14
.= Sum (th rExpSeq) by Lm9
.= exp_R th by Def22 ; :: thesis: verum