dom (f - f) = (dom f) /\ (dom f) by VALUED_1:12;
hence f - f is total by PARTFUN1:def 2; :: thesis: verum