let y be Real; :: thesis: ( y > 0 implies exp_R (log (number_e,y)) = y )
assume y > 0 ; :: thesis: exp_R (log (number_e,y)) = y
then number_e to_power (log (number_e,y)) = y by Lm4, POWER:def 3;
hence exp_R (log (number_e,y)) = y by Th9; :: thesis: verum