for x being Real holds log (number_e,(exp_R x)) = x