let y be real number ; :: 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