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) = (- 1r) (#) (f / g) by COMPLEX1:def 4
.= (- f) / g by Th52, COMPLEX1:def 4 ; :: thesis: f / (- g) = - (f / g)
thus f / (- g) = f (#) ((- g) ^) by Th51
.= f (#) ((- 1r) (#) (g ^)) by Lm2, Th46, COMPLEX1:def 4
.= - (f (#) (g ^)) by Th27, COMPLEX1:def 4
.= - (f / g) by Th51 ; :: thesis: verum