theorem :: SIN_COS3:55

for x, y being Element of REAL holds (((1 + ((- 1) * <i>)) / 2) * (cosh_C /. (x + (y * <i>)))) + (((1 + <i>) / 2) * (cosh_C /. (x + ((- y) * <i>)))) = ((sinh . x) * (sin . y)) + ((cosh . x) * (cos . y))