let z be Complex; :: thesis: - (sin_C /. z) = sin_C /. (- z)
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