theorem Th15: :: TAYLOR_1:15

for y being Real st y > 0 holds
exp_R . (log (number_e,y)) = y