theorem Th1: :: FDIFF_6:1

for x, a being Real st a > 0 holds
exp_R . (x * (log (number_e,a))) = a #R x