let f1, f, g1, g be complex-valued Function; :: thesis: (f1 / f) - (g1 / g) = ((f1 (#) g) - (g1 (#) f)) / (f (#) g)
thus (f1 / f) - (g1 / g) = (f1 / f) + (((- 1) (#) g1) / g) by Th48
.= ((f1 (#) g) + (((- 1) (#) g1) (#) f)) / (f (#) g) by Th56
.= ((f1 (#) g) - (g1 (#) f)) / (f (#) g) by Th24 ; :: thesis: verum