theorem :: CFUNCT_1:49

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