theorem :: SIN_COS2:21

for p, r being Real holds
( sinh . (p + r) = ((sinh . p) * (cosh . r)) + ((cosh . p) * (sinh . r)) & sinh . (p - r) = ((sinh . p) * (cosh . r)) - ((cosh . p) * (sinh . r)) ) by Lm3, Lm8;