theorem Th12: :: TAYLOR_1:12

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