let C be non empty set ; :: thesis: for f, g being PartFunc of C,COMPLEX holds
( - (f / g) = (- f) / g & f / (- g) = - (f / g) )
let f, g be PartFunc of C,COMPLEX; :: thesis: ( - (f / g) = (- f) / g & f / (- g) = - (f / g) )
thus - (f / g) = (- f) / g by Th39; :: thesis: f / (- g) = - (f / g)
thus f / (- g) = f (#) ((- g) ^) by Th38
.= f (#) ((- 1r) (#) (g ^)) by Lm2, Th35, COMPLEX1:def 4
.= - (f (#) (g ^)) by Th18, COMPLEX1:def 4
.= - (f / g) by Th38 ; :: thesis: verum