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