theorem Th13: :: TAYLOR_1:13

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