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