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

let x be object ; :: thesis: ( x in {<*1,2,3*>,<*3,2,1*>,<*1,3,2*>,<*2,3,1*>,<*2,1,3*>,<*3,1,2*>} implies x in Permutations 3 )
A1: idseq 3 in Permutations 3 by MATRIX_1:def 12;
A2: <*3,1,2*> in Permutations 3

proof

reconsider h = <*1,2*> as FinSequence of NAT ;
<*3*> ^ h = <*3,1,2*> by FINSEQ_1:43;
hence <*3,1,2*> in Permutations 3 by A1, Th18, FINSEQ_2:53; :: thesis: verum

end;

A3: <*2,3,1*> in Permutations 3

proof

reconsider h = <*2,3*> as FinSequence of NAT ;
reconsider f = <*1,2,3*> as one-to-one FinSequence-like Function of (Seg 3),(Seg 3) by FINSEQ_2:53;
f = <*1*> ^ h by FINSEQ_1:43;
hence <*2,3,1*> in Permutations 3 by A1, Th18, FINSEQ_2:53; :: thesis: verum

end;

A4: <*1,3,2*> in Permutations 3

proof

reconsider h = <*2,3*> as FinSequence of NAT ;
reconsider f = <*1,2,3*> as one-to-one FinSequence-like Function of (Seg 3),(Seg 3) by FINSEQ_2:53;
Rev h = <*3,2*> by FINSEQ_5:61;
then ( f = <*1*> ^ h & <*1*> ^ (Rev h) = <*1,3,2*> ) by FINSEQ_1:43;
hence <*1,3,2*> in Permutations 3 by A1, Th17, FINSEQ_2:53; :: thesis: verum

end;

A5: <*2,1,3*> in Permutations 3

proof

reconsider h = <*1,2*> as FinSequence of NAT ;
<*3*> ^ h in Permutations 3 by A1, Th18, FINSEQ_2:53;
then ( Rev h = <*2,1*> & <*3*> ^ (Rev h) in Permutations 3 ) by Th17, FINSEQ_5:61;
hence <*2,1,3*> in Permutations 3 by Th18; :: thesis: verum

end;

assume x in {<*1,2,3*>,<*3,2,1*>,<*1,3,2*>,<*2,3,1*>,<*2,1,3*>,<*3,1,2*>} ; :: thesis: x in Permutations 3
then x in {<*1,2,3*>,<*3,2,1*>} \/ {<*1,3,2*>,<*2,3,1*>,<*2,1,3*>,<*3,1,2*>} by ENUMSET1:12;
then ( x in {<*1,2,3*>,<*3,2,1*>} or x in {<*1,3,2*>,<*2,3,1*>,<*2,1,3*>,<*3,1,2*>} ) by XBOOLE_0:def 3;
then ( x in {<*1,2,3*>,<*3,2,1*>} or x in {<*1,3,2*>,<*2,3,1*>} \/ {<*2,1,3*>,<*3,1,2*>} ) by ENUMSET1:5;
then A6: ( x in {<*1,2,3*>,<*3,2,1*>} or x in {<*1,3,2*>,<*2,3,1*>} or x in {<*2,1,3*>,<*3,1,2*>} ) by XBOOLE_0:def 3;
Rev (idseq 3) in Permutations 3 by Th4;
hence x in Permutations 3 by A6, A1, A4, A3, A5, A2, Th15, FINSEQ_2:53, TARSKI:def 2; :: thesis: verum

end;

then A7: {<*1,2,3*>,<*3,2,1*>,<*1,3,2*>,<*2,3,1*>,<*2,1,3*>,<*3,1,2*>} c= Permutations 3 by TARSKI:def 3;

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

let p be object ; :: thesis: ( p in Permutations 3 implies p in {<*1,2,3*>,<*3,2,1*>,<*1,3,2*>,<*2,3,1*>,<*2,1,3*>,<*3,1,2*>} )
assume p in Permutations 3 ; :: thesis: p in {<*1,2,3*>,<*3,2,1*>,<*1,3,2*>,<*2,3,1*>,<*2,1,3*>,<*3,1,2*>}
then reconsider q = p as Permutation of (Seg 3) by MATRIX_1:def 12;
A8: rng q = Seg 3 by FUNCT_2:def 3;
A9: 3 in Seg 3 ;
then q . 3 in Seg 3 by A8, FUNCT_2:4;
then A10: ( q . 3 = 1 or q . 3 = 2 or q . 3 = 3 ) by ENUMSET1:def 1, FINSEQ_3:1;
A11: 2 in Seg 3 ;
then q . 2 in Seg 3 by A8, FUNCT_2:4;
then A12: ( q . 2 = 1 or q . 2 = 2 or q . 2 = 3 ) by ENUMSET1:def 1, FINSEQ_3:1;
A13: dom q = Seg 3 by FUNCT_2:52;
A14: ( ( not ( q . 1 = 1 & q . 2 = 2 & q . 3 = 3 ) & not ( q . 1 = 3 & q . 2 = 2 & q . 3 = 1 ) & not ( q . 1 = 1 & q . 2 = 3 & q . 3 = 2 ) & not ( q . 1 = 2 & q . 2 = 3 & q . 3 = 1 ) & not ( q . 1 = 2 & q . 2 = 1 & q . 3 = 3 ) & not ( q . 1 = 3 & q . 2 = 1 & q . 3 = 2 ) ) or q = <*1,2,3*> or q = <*3,2,1*> or q = <*1,3,2*> or q = <*2,3,1*> or q = <*2,1,3*> or q = <*3,1,2*> )

proof

reconsider q = q as FinSequence by A13, FINSEQ_1:def 2;
len q = 3 by A13, FINSEQ_1:def 3;
hence ( ( not ( q . 1 = 1 & q . 2 = 2 & q . 3 = 3 ) & not ( q . 1 = 3 & q . 2 = 2 & q . 3 = 1 ) & not ( q . 1 = 1 & q . 2 = 3 & q . 3 = 2 ) & not ( q . 1 = 2 & q . 2 = 3 & q . 3 = 1 ) & not ( q . 1 = 2 & q . 2 = 1 & q . 3 = 3 ) & not ( q . 1 = 3 & q . 2 = 1 & q . 3 = 2 ) ) or q = <*1,2,3*> or q = <*3,2,1*> or q = <*1,3,2*> or q = <*2,3,1*> or q = <*2,1,3*> or q = <*3,1,2*> ) by FINSEQ_1:45; :: thesis: verum

end;

A15: 1 in Seg 3 ;
then q . 1 in Seg 3 by A8, FUNCT_2:4;
then ( q . 1 = 1 or q . 1 = 2 or q . 1 = 3 ) by ENUMSET1:def 1, FINSEQ_3:1;
then ( p = <*1,2,3*> or p = <*3,2,1*> or q = <*1,3,2*> or q = <*2,3,1*> or q = <*2,1,3*> or q = <*3,1,2*> ) by A13, A15, A11, A9, A12, A10, A14, FUNCT_1:def 4;
then ( p in {<*1,2,3*>,<*3,2,1*>} or q in {<*1,3,2*>,<*2,3,1*>} or q in {<*2,1,3*>,<*3,1,2*>} ) by TARSKI:def 2;
then ( p in {<*1,2,3*>,<*3,2,1*>} or q in {<*1,3,2*>,<*2,3,1*>} \/ {<*2,1,3*>,<*3,1,2*>} ) by XBOOLE_0:def 3;
then ( p in {<*1,2,3*>,<*3,2,1*>} or q in {<*1,3,2*>,<*2,3,1*>,<*2,1,3*>,<*3,1,2*>} ) by ENUMSET1:5;
then p in {<*1,2,3*>,<*3,2,1*>} \/ {<*1,3,2*>,<*2,3,1*>,<*2,1,3*>,<*3,1,2*>} by XBOOLE_0:def 3;
hence p in {<*1,2,3*>,<*3,2,1*>,<*1,3,2*>,<*2,3,1*>,<*2,1,3*>,<*3,1,2*>} by ENUMSET1:12; :: thesis: verum

end;

then Permutations 3 c= {<*1,2,3*>,<*3,2,1*>,<*1,3,2*>,<*2,3,1*>,<*2,1,3*>,<*3,1,2*>} by TARSKI:def 3;
hence Permutations 3 = {<*1,2,3*>,<*3,2,1*>,<*1,3,2*>,<*2,3,1*>,<*2,1,3*>,<*3,1,2*>} by A7, XBOOLE_0:def 10; :: thesis: verum