theorem :: SIN_COS7:44

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