theorem Th42: :: SIN_COS3:42

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