theorem :: FOMODEL0:78

for X being set
for f being Function st X c= f holds
dom (f \ X) = (dom f) \ (proj1 X) by Lm71;