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