let y be real number ; :: 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 27
.= y by A1, Th14 ; :: thesis: verum