let f, f1, g, g1 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 Th32
.= ((f1 (#) g) + (((- 1) (#) g1) (#) f)) / (f (#) g) by Th40
.= ((f1 (#) g) - (g1 (#) f)) / (f (#) g) by Th12 ; :: thesis: verum