theorem :: RFUNCT_1:37
for f1, f2, g being complex-valued Function holds g / (f1 / f2) = (g (#) (f2 | (dom (f2 ^)))) / f1