let z be Complex; :: thesis: - (sinh_C /. z) = sinh_C /. (- z)
sinh_C /. (- z) = ((exp (- z)) - (exp (- (- z)))) / 2 by Def3
.= - (((exp z) - (exp (- z))) / 2) ;
hence - (sinh_C /. z) = sinh_C /. (- z) by Def3; :: thesis: verum