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 ; :: 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 ; :: 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 ; :: 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 ;
then ( Rev h = <*2,1*> & <*3*> ^ (Rev h) in Permutations 3 ) by ;
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:
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 () in Permutations 3 by Th4;
hence x in Permutations 3 by ; :: 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 ;
then A10: ( q . 3 = 1 or q . 3 = 2 or q . 3 = 3 ) by ;
A11: 2 in Seg 3 ;
then q . 2 in Seg 3 by ;
then A12: ( q . 2 = 1 or q . 2 = 2 or q . 2 = 3 ) by ;
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 ;
len q = 3 by ;
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 ;
then ( q . 1 = 1 or q . 1 = 2 or q . 1 = 3 ) by ;
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 ;
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 ; :: thesis: verum