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