theorem :: FUNCT_4:120
for f, g being Function st dom f misses dom g holds
f \ g = f by RELAT_1:179, XBOOLE_1:83;