A1: idseq 3 in Permutations 3 by MATRIX_2:def 11;
reconsider f = <*1,2,3*> as one-to-one FinSequence-like Function of (Seg 3),(Seg 3) by FINSEQ_2:62;
A2: <*1,3,2*> in Permutations 3

proof

set h = <*2,3*>;
A3: f = <*1*> ^ <*2,3*> by FINSEQ_1:60;
A4: f in Permutations 3 by FINSEQ_2:62, MATRIX_2:def 11;
Rev <*2,3*> = <*3,2*> by FINSEQ_5:64;
then <*1*> ^ (Rev <*2,3*>) = <*1,3,2*> by FINSEQ_1:60;
hence <*1,3,2*> in Permutations 3 by A3, A4, Th17; :: thesis: verum

end;

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

proof

f = <*1*> ^ <*2,3*> by FINSEQ_1:60;
hence <*2,3,1*> in Permutations 3 by A1, Th18, FINSEQ_2:62; :: thesis: verum

end;

set h = <*1,2*>;
A6: <*2,1,3*> in Permutations 3

proof

A7: <*3*> ^ <*1,2*> in Permutations 3 by A1, Th18, FINSEQ_2:62;
A8: Rev <*1,2*> = <*2,1*> by FINSEQ_5:64;
<*3*> ^ (Rev <*1,2*>) in Permutations 3 by A7, Th17;
hence <*2,1,3*> in Permutations 3 by A8, Th18; :: thesis: verum

end;

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

proof

<*3*> ^ <*1,2*> = <*3,1,2*> by FINSEQ_1:60;
hence <*3,1,2*> in Permutations 3 by A1, Th18, FINSEQ_2:62; :: thesis: verum

end;

hence ( <*1,3,2*> in Permutations 3 & <*2,3,1*> in Permutations 3 & <*2,1,3*> in Permutations 3 & <*3,1,2*> in Permutations 3 & <*1,2,3*> in Permutations 3 & <*3,2,1*> in Permutations 3 ) by A1, A2, A5, A6, Th5, Th15, FINSEQ_2:62; :: thesis: verum