let C be non empty set ; :: thesis: for f, f1, g, g1 being PartFunc of C,COMPLEX holds (f1 / f) - (g1 / g) = ((f1 (#) g) - (g1 (#) f)) / (f (#) g)
let f, f1, g, g1 be PartFunc of C,COMPLEX; :: thesis: (f1 / f) - (g1 / g) = ((f1 (#) g) - (g1 (#) f)) / (f (#) g)
thus (f1 / f) - (g1 / g) = (f1 / f) + (((- 1r) (#) g1) / g) by Th39, COMPLEX1:def 4
.= ((f1 (#) g) + (((- 1r) (#) g1) (#) f)) / (f (#) g) by Th47
.= ((f1 (#) g) - (g1 (#) f)) / (f (#) g) by Th17, COMPLEX1:def 4 ; :: thesis: verum