theorem :: SIN_COS7:43

for x being Real st x ^2 < 1 holds
tanh" x = (1 / 2) * (sinh" ((2 * x) / (1 - (x ^2))))