dom (Homogen f) = dom f by DomHomogen;
hence not Homogen f is empty ; :: thesis: verum