let x be Real; :: thesis: log (number_e,(exp_R . x)) = x
thus log (number_e,(exp_R . x)) = log (number_e,(exp_R x)) by SIN_COS:def 23
.= x by Th12 ; :: thesis: verum