theorem :: SIN_COS7:57

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