dom (Swap f,i,j) = dom f by FUNCT_7:101;
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