let x, y be Real; :: thesis: sinh_C /. (x + ((- y) * <i>)) = ((sinh . x) * (cos . y)) + ((- ((cosh . x) * (sin . y))) * <i>)
sinh_C /. (x + ((- y) * <i>)) = ((sinh . x) * (cos . (- y))) + (((cosh . x) * (sin . (- y))) * <i>) by Th46
.= ((sinh . x) * (cos . y)) + (((cosh . x) * (sin . (- y))) * <i>) by SIN_COS:30
.= ((sinh . x) * (cos . y)) + (((cosh . x) * (- (sin . y))) * <i>) by SIN_COS:30 ;
hence sinh_C /. (x + ((- y) * <i>)) = ((sinh . x) * (cos . y)) + ((- ((cosh . x) * (sin . y))) * <i>) ; :: thesis: verum