theorem Th48: :: SIN_COS3:48
for x, y being Real holds cosh_C /. (x + (y * <i>)) = ((cosh . x) * (cos . y)) + (((sinh . x) * (sin . y)) * <i>)