for x being Real holds
( (exp_R 1) #R x = exp_R x & (exp_R 1) to_power x = exp_R x & number_e to_power x = exp_R x & number_e #R x = exp_R x )