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