dom (Swap (f,i,j)) = dom f by FUNCT_7:99;
hence ex n being Nat st dom (Swap (f,i,j)) = Seg n by FINSEQ_1:def 2; :: according to FINSEQ_1:def 2 :: thesis: verum