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