theorem :: SIN_COS3:62

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