for x being Real holds
( exp_R x = (cosh x) + (sinh x) & exp_R (- x) = (cosh x) - (sinh x) & exp_R x = ((cosh (x / 2)) + (sinh (x / 2))) / ((cosh (x / 2)) - (sinh (x / 2))) & exp_R (- x) = ((cosh (x / 2)) - (sinh (x / 2))) / ((cosh (x / 2)) + (sinh (x / 2))) & exp_R x = (1 + (tanh (x / 2))) / (1 - (tanh (x / 2))) & exp_R (- x) = (1 - (tanh (x / 2))) / (1 + (tanh (x / 2))) )