let f, g be complex-valued Function; :: thesis: ( - (f / g) = (- f) / g & f / (- g) = - (f / g) )
thus - (f / g) = (- f) / g by Th48; :: thesis: f / (- g) = - (f / g)
thus f / (- g) = f (#) ((- g) ^) by Th47
.= f (#) ((- 1) (#) (g ^)) by Lm1, Th44
.= - (f (#) (g ^)) by Th25
.= - (f / g) by Th47 ; :: thesis: verum