let x, y be Element of REAL ; :: thesis: cosh_C /. (x + ((- y) * <i> )) = ((cosh . x) * (cos . y)) + ((- ((sinh . x) * (sin . y))) * <i> )
cosh_C /. (x + ((- y) * <i> )) = ((cosh . x) * (cos . (- y))) + (((sinh . x) * (sin . (- y))) * <i> ) by Th49
.= ((cosh . x) * (cos . y)) + (((sinh . x) * (sin . (- y))) * <i> ) by SIN_COS:33
.= ((cosh . x) * (cos . y)) + (((sinh . x) * (- (sin . y))) * <i> ) by SIN_COS:33 ;
hence cosh_C /. (x + ((- y) * <i> )) = ((cosh . x) * (cos . y)) + ((- ((sinh . x) * (sin . y))) * <i> ) ; :: thesis: verum