theorem :: CFUNCT_1:45

for C being non empty set
for f1, f2, g being PartFunc of C,COMPLEX holds g / (f1 / f2) = (g (#) (f2 | (dom (f2 ^)))) / f1