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