theorem :: SIN_COS7:68

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