rng (Swap (f,x,y)) = rng f by FUNCT_7:103;
hence rng (Swap (f,x,y)) = X by FUNCT_2:def 3; :: according to FUNCT_2:def 3 :: thesis: verum