let x be real number ; :: thesis: log number_e ,(exp_R x) = x
( exp_R x > 0 & number_e to_power x = exp_R x ) by Th9, SIN_COS:60;
hence log number_e ,(exp_R x) = x by Lm4, POWER:def 3; :: thesis: verum