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