rng (Swap (f,i,j)) = rng f by FUNCT_7:103;
hence rng (Swap (f,i,j)) c= D by FINSEQ_1:def 4; :: according to FINSEQ_1:def 4 :: thesis: verum