let f be Permutation of (Seg 2); :: thesis: ( f = <*1,2*> or f = <*2,1*> )
A1: rng f = Seg 2 by FUNCT_2:def 3;
2 in {1,2} by TARSKI:def 2;
then A2: f . 2 in Seg 2 by A1, FINSEQ_1:2, FUNCT_2:4;
A3: dom f = Seg 2 by FUNCT_2:52;
then reconsider p = f as FinSequence by FINSEQ_1:def 2;
A4: len p = 2 by A3, FINSEQ_1:def 3;
A5: ( 1 in dom f & 2 in dom f ) by A3;
1 in {1,2} by TARSKI:def 2;
then A6: f . 1 in Seg 2 by A1, FINSEQ_1:2, FUNCT_2:4;

now :: thesis: ( ( f . 1 = 1 & f . 2 = 1 & contradiction ) or ( f . 1 = 1 & f . 2 = 2 & ( f = <*1,2*> or f = <*2,1*> ) ) or ( f . 1 = 2 & f . 2 = 1 & ( f = <*1,2*> or f = <*2,1*> ) ) or ( f . 1 = 2 & f . 2 = 2 & contradiction ) )

per cases ( ( f . 1 = 1 & f . 2 = 1 ) or ( f . 1 = 1 & f . 2 = 2 ) or ( f . 1 = 2 & f . 2 = 1 ) or ( f . 1 = 2 & f . 2 = 2 ) ) by A6, A2, FINSEQ_1:2, TARSKI:def 2;

case ( f . 1 = 1 & f . 2 = 1 ) ; :: thesis: contradiction

hence contradiction by A5, FUNCT_1:def 4; :: thesis: verum

end;

case ( f . 1 = 1 & f . 2 = 2 ) ; :: thesis: ( f = <*1,2*> or f = <*2,1*> )

hence ( f = <*1,2*> or f = <*2,1*> ) by A4, FINSEQ_1:44; :: thesis: verum

end;

case ( f . 1 = 2 & f . 2 = 1 ) ; :: thesis: ( f = <*1,2*> or f = <*2,1*> )

hence ( f = <*1,2*> or f = <*2,1*> ) by A4, FINSEQ_1:44; :: thesis: verum

end;

case ( f . 1 = 2 & f . 2 = 2 ) ; :: thesis: contradiction

hence contradiction by A5, FUNCT_1:def 4; :: thesis: verum

end;

end;

end;

hence ( f = <*1,2*> or f = <*2,1*> ) ; :: thesis: verum