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