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

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

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

A4:
idseq 3 in Permutations 3
by MATRIX_1:def 12;
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;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

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