let z be Complex; :: thesis: cosh_C /. z = cosh_C /. (- z)
cosh_C /. (- z) = ((exp (- z)) + (exp (- (- z)))) / 2 by Def4
.= ((exp (- z)) + (exp z)) / 2 ;
hence cosh_C /. z = cosh_C /. (- z) by Def4; :: thesis: verum