let x, y be Element of 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 Th47
.= ((sinh . x) * (cos . y)) + (((cosh . x) * (sin . (- y))) * <i> ) by SIN_COS:33
.= ((sinh . x) * (cos . y)) + (((cosh . x) * (- (sin . y))) * <i> ) by SIN_COS:33 ;
hence sinh_C /. (x + ((- y) * <i> )) = ((sinh . x) * (cos . y)) + ((- ((cosh . x) * (sin . y))) * <i> ) ; :: thesis: verum