theorem :: SIN_COS7:65

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