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