theorem Th45: :: SIN_COS3:45

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