let y be Real; :: thesis: ( y > 0 implies exp_R . (log (number_e,y)) = y )
assume A1: y > 0 ; :: thesis: exp_R . (log (number_e,y)) = y
thus exp_R . (log (number_e,y)) = exp_R (log (number_e,y)) by SIN_COS:def 23
.= y by A1, Th14 ; :: thesis: verum