dom (f - f) = (dom f) /\ (dom f) by VALUED_1:12;
hence f - f is dom f -defined by RELAT_1:def 18; :: thesis: verum