theorem :: SIN_COS7:56

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