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