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 )