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