( ln = exp_R " & ln is one-to-one & dom ln = right_open_halfline 0 & rng ln = REAL & ln is_differentiable_on right_open_halfline 0 & ( for x being Real st x > 0 holds
ln is_differentiable_in x ) & ( for x being Element of right_open_halfline 0 holds diff (ln,x) = 1 / x ) & ( for x being Element of right_open_halfline 0 holds 0 < diff (ln,x) ) )