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

now

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 A3, A8, FINSEQ_1:4, TARSKI:def 2;

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

hence contradiction by A6, A7, FUNCT_1:def 8; :: 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 A5, FINSEQ_1:61; :: 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 A5, FINSEQ_1:61; :: thesis: verum

end;

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

hence contradiction by A6, A7, FUNCT_1:def 8; :: thesis: verum

end;

end;

end;

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