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