theorem :: CFUNCT_1:50

for C being non empty set
for f, f1, g, g1 being PartFunc of C,COMPLEX holds (f1 / f) - (g1 / g) = ((f1 (#) g) - (g1 (#) f)) / (f (#) g)