consider x being Element of f;
ex x1, x2 being set st x = [x1,x2] by Def1;
hence not rng f is empty by Def5; :: thesis: verum