theorem Th24: :: SIN_COS2:24

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