let x be Real; :: thesis: ln . (exp_R . x) = x
A1: exp_R . x in right_open_halfline 0 by XXREAL_1:235, SIN_COS:54;
log (number_e,(exp_R . x)) = x by TAYLOR_1:13;
hence ln . (exp_R . x) = x by A1, TAYLOR_1:def 3, TAYLOR_1:def 2; :: thesis: verum