theorem :: RFUNCT_1:42

for f, f1, g, g1 being complex-valued Function holds (f1 / f) - (g1 / g) = ((f1 (#) g) - (g1 (#) f)) / (f (#) g)