theorem Th3: :: PARTFUN3:3

for X being set
for f being PartFunc of X,REAL
for g being non-empty PartFunc of X,REAL holds dom (f / g) = (dom f) /\ (dom g)