theorem :: SIN_COS7:45

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