A1: ( dom (Swap (f,a,b)) = dom f & dom f = Seg (len f) ) by Def4, FINSEQ_1:def 3;
then reconsider S = Swap (f,a,b) as FinSequence by FINSEQ_1:def 2;
len S = len f by A1, FINSEQ_3:29;
hence ( Swap (f,a,b) is len f -element & Swap (f,a,b) is FinSequence-like ) by CARD_1:def 7; :: thesis: verum