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