for p, x being Real holds (exp_R x) #R p = exp_R (p * x)