let x, y be Real; :: thesis: sin_C /. (x + ((- y) * <i>)) = ((sin . x) * (cosh . y)) + ((- ((cos . x) * (sinh . y))) * <i>)
sin_C /. (x + ((- y) * <i>)) = ((sin . x) * (cosh . (- y))) + (((cos . x) * (sinh . (- y))) * <i>) by Th42
.= ((sin . x) * (cosh . y)) + (((cos . x) * (sinh . (- y))) * <i>) by SIN_COS2:19
.= ((sin . x) * (cosh . y)) + (((cos . x) * (- (sinh . y))) * <i>) by SIN_COS2:19 ;
hence sin_C /. (x + ((- y) * <i>)) = ((sin . x) * (cosh . y)) + ((- ((cos . x) * (sinh . y))) * <i>) ; :: thesis: verum