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