theorem :: SIN_COS2:26

for p, r being Real holds
( (sinh . p) + (sinh . r) = (2 * (sinh . ((p / 2) + (r / 2)))) * (cosh . ((p / 2) - (r / 2))) & (sinh . p) - (sinh . r) = (2 * (sinh . ((p / 2) - (r / 2)))) * (cosh . ((p / 2) + (r / 2))) )