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