let z be Complex; :: thesis: cosh_C /. (<i> * z) = cos_C /. z
reconsider z = z as Element of COMPLEX by XCMPLX_0:def 2;
cosh_C /. (<i> * z) = ((exp (<i> * z)) + (exp (- (<i> * z)))) / 2 by Def4;
then cosh_C /. (<i> * z) = cos_C /. z by Def2;
hence cosh_C /. (<i> * z) = cos_C /. z ; :: thesis: verum