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