theorem Th25: :: SIN_COS2:25

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