theorem Th4: :: TAYLOR_1:4

for x being Real holds exp_R (- x) = 1 / (exp_R x)