now :: thesis: for x being object st x in {(idseq 2),<*2,1*>} holds
x in Permutations 2

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

now :: thesis: ( ( x = idseq 2 & x in Permutations 2 ) or ( x = <*2,1*> & x in Permutations 2 ) )

per cases ( x = idseq 2 or x = <*2,1*> ) by A1, TARSKI:def 2;

case x = idseq 2 ; :: thesis: x in Permutations 2

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

end;

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

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

end;

end;

end;

hence x in Permutations 2 ; :: thesis: verum

end;

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

now :: thesis: for p being object st p in Permutations 2 holds
p in {(idseq 2),<*2,1*>}

let p be object ; :: thesis: ( p in Permutations 2 implies p in {(idseq 2),<*2,1*>} )
assume p in Permutations 2 ; :: thesis: p in {(idseq 2),<*2,1*>}
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: verum

end;

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