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