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