theorem :: SIN_COS8:33

for y, z being Real holds
( (cosh (2 * y)) + (cos (2 * z)) = 2 + (2 * (((sinh y) ^2) - ((sin z) ^2))) & (cosh (2 * y)) - (cos (2 * z)) = 2 * (((sinh y) ^2) + ((sin z) ^2)) )