( dom (doms f) = dom f & dom f <> {} ) by FUNCT_6:def 2;
hence not doms f is empty ; :: thesis: verum