set g = Swap (f,x,y);
A1: dom f = X by FUNCT_2:def 1;
A2: ( dom (Swap (f,x,y)) = dom f & rng (Swap (f,x,y)) = rng f ) by FUNCT_7:99, FUNCT_7:103;
rng f c= Y by RELAT_1:def 19;
hence Swap (f,x,y) is Function of X,Y by A1, A2, FUNCT_2:2; :: thesis: verum