ex x1, x2 being set st the Element of f = [x1,x2] by Def1;
hence not dom f is empty by Def4; :: thesis: verum