let a, b be Complex; :: thesis: a / (- b) = - (a / b)
a / (- b) = (a * (- 1)) / ((- b) * (- 1)) by Lm10;
then a / (- b) = (- a) / ((- (- b)) * 1)
.= - (a / b) by Lm17 ;
hence a / (- b) = - (a / b) ; :: thesis: verum