theorem :: SIN_COS7:66

for x, y being Real st y = ((exp_R x) + (exp_R (- x))) / ((exp_R x) - (exp_R (- x))) & x <> 0 holds
x = (1 / 2) * (log (number_e,((y + 1) / (y - 1))))