theorem :: SIN_COS7:42

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