let C be non empty set ; :: thesis: for f1, f, g1, g being PartFunc of C,COMPLEX holds (f1 / f) - (g1 / g) = ((f1 (#) g) - (g1 (#) f)) / (f (#) g)
let f1, f, g1, g 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 Th52, COMPLEX1:def 4
.= ((f1 (#) g) + (((- 1r) (#) g1) (#) f)) / (f (#) g) by Th60
.= ((f1 (#) g) - (g1 (#) f)) / (f (#) g) by Th26, COMPLEX1:def 4 ; :: thesis: verum