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

proof

set h = <*2,3*>;
Rev <*2,3*> = <*3,2*> by FINSEQ_5:61;
then A3: <*1*> ^ (Rev <*2,3*>) = <*1,3,2*> by FINSEQ_1:43;
( f = <*1*> ^ <*2,3*> & f in Permutations 3 ) by FINSEQ_1:43, FINSEQ_2:53, MATRIX_1:def 12;
hence <*1,3,2*> in Permutations 3 by A3, Th17; :: thesis: verum

end;

A4: idseq 3 in Permutations 3 by MATRIX_1:def 12;
then <*3*> ^ <*1,2*> in Permutations 3 by Th18, FINSEQ_2:53;
then A5: <*3*> ^ (Rev <*1,2*>) in Permutations 3 by Th17;
( f = <*1*> ^ <*2,3*> & Rev <*1,2*> = <*2,1*> ) by FINSEQ_1:43, FINSEQ_5:61;
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 A4, A2, A5, A1, Th5, Th15, Th18, FINSEQ_2:53; :: thesis: verum