theorem Th49: :: SIN_COS3:49

for x, y being Real holds cosh_C /. (x + ((- y) * <i>)) = ((cosh . x) * (cos . y)) + ((- ((sinh . x) * (sin . y))) * <i>)