theorem Th35: :: RFUNCT_1:35

for f1, f2 being complex-valued Function holds (f1 / f2) ^ = (f2 | (dom (f2 ^))) / f1