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