theorem Th5: :: TAYLOR_1:5
for i being Integer
for x being Real holds (exp_R x) #R (1 / i) = exp_R (x / i)