let z be complex number ; :: thesis: cosh_C /. z = ((exp z) + (exp (- z))) / 2
reconsider z = z as Element of COMPLEX by XCMPLX_0:def 2;
cosh_C /. z = ((exp z) + (exp (- z))) / 2 by Def4;
hence cosh_C /. z = ((exp z) + (exp (- z))) / 2 ; :: thesis: verum