theorem :: SIN_COS2:20

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