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