theorem Th57: :: SIN_COS3:57

for z being Complex holds (cosh_C /. z) * (cosh_C /. z) = ((cosh_C /. (2 * z)) + 1) / 2