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