let f, g be Function; :: thesis: ( dom f misses dom g implies f \ g = f )
assume dom f misses dom g ; :: thesis: f \ g = f
then f misses g by RELAT_1:179;
hence f \ g = f by XBOOLE_1:83; :: thesis: verum