theorem :: SIN_COS7:37

for x being Real st x > 1 holds
cosh1" x = tanh" ((sqrt ((x ^2) - 1)) / x)