theorem Th8: :: TAYLOR_1:8

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