let f, g be complex-valued Function; :: thesis: ( - (f / g) = (- f) / g & f / (- g) = - (f / g) )
thus - (f / g) = (- f) / g by Th32; :: thesis: f / (- g) = - (f / g)
thus f / (- g) = f (#) ((- g) ^) by Th31
.= f (#) ((- 1) (#) (g ^)) by Lm1, Th28
.= - (f (#) (g ^)) by Th13
.= - (f / g) by Th31 ; :: thesis: verum