let x, y be Element of 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 Th46; :: thesis: verum