theorem Th60: :: SIN_COS3:60

for z1, z2 being Complex holds
( (cosh_C /. (z1 + z2)) * (cosh_C /. (z1 - z2)) = ((sinh_C /. z1) * (sinh_C /. z1)) + ((cosh_C /. z2) * (cosh_C /. z2)) & (cosh_C /. (z1 + z2)) * (cosh_C /. (z1 - z2)) = ((cosh_C /. z1) * (cosh_C /. z1)) + ((sinh_C /. z2) * (sinh_C /. z2)) & ((sinh_C /. z1) * (sinh_C /. z1)) + ((cosh_C /. z2) * (cosh_C /. z2)) = ((cosh_C /. z1) * (cosh_C /. z1)) + ((sinh_C /. z2) * (sinh_C /. z2)) )