now :: thesis:

let x be object ; :: thesis:
assume A1: x in {(idseq 2),<*2,1*>} ; :: thesis:

now :: thesis:

per cases by A1, TARSKI:def 2;

case x = idseq 2 ; :: thesis:

hence x in Permutations 2 by MATRIX_1:def 12; :: thesis:

end;

case A2: x = <*2,1*> ; :: thesis:

<*2,1*> is Permutation of (Seg 2) by Th2;
hence x in Permutations 2 by A2, MATRIX_1:def 12; :: thesis:

end;

end;

end;

hence x in Permutations 2 ; :: thesis:

end;

then A3: {(idseq 2),<*2,1*>} c= Permutations 2 ;

now :: thesis:

let p be object ; :: thesis:
assume p in Permutations 2 ; :: thesis:
then reconsider q = p as Permutation of (Seg 2) by MATRIX_1:def 12;
( q = <*1,2*> or q = <*2,1*> ) by Th1;
hence p in {(idseq 2),<*2,1*>} by FINSEQ_2:52, TARSKI:def 2; :: thesis:

end;

then Permutations 2 c= {(idseq 2),<*2,1*>} ;
hence Permutations 2 = {<*1,2*>,<*2,1*>} by A3, FINSEQ_2:52; :: thesis: