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