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