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