theorem :: CFUNCT_1:41

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