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