let x be real number ; :: 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 27
.= x by Th12 ; :: thesis: verum