theorem :: SIN_COS7:63

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