theorem Th47: :: SIN_COS3:47

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