theorem :: SIN_COS2:22

for p, r being Real holds
( tanh . (p + r) = ((tanh . p) + (tanh . r)) / (1 + ((tanh . p) * (tanh . r))) & tanh . (p - r) = ((tanh . p) - (tanh . r)) / (1 - ((tanh . p) * (tanh . r))) ) by Lm5, Lm9;