let f be FinSequence; :: thesis:
assume A1: ( f = <*1,2*> or f = <*2,1*> ) ; :: thesis:
( len <*1,2*> = 2 & len <*2,1*> = 2 ) by FINSEQ_1:44;
then A2: dom f = Seg 2 by A1, FINSEQ_1:def 3;
rng f c= Seg 2

proof

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume y in rng f ; :: thesis:
then ex x being object st
( x in dom f & y = f . x ) by FUNCT_1:def 3;
then ( y = f . 1 or y = f . 2 ) by A2, FINSEQ_1:2, TARSKI:def 2;
then ( y = 1 or y = 2 or y = 2 or y = 1 ) by A1, FINSEQ_1:44;
hence y in Seg 2 ; :: thesis:

end;

then reconsider g = f as Function of (Seg 2),(Seg 2) by A2, FUNCT_2:2;

now :: thesis:

per cases by A1;

case A3: f = <*1,2*> ; :: thesis:

for x1, x2 being object st x1 in dom f & x2 in dom f & f . x1 = f . x2 holds
x1 = x2

proof

let x1, x2 be object ; :: thesis:
assume that
A4: ( x1 in dom f & x2 in dom f ) and
A5: f . x1 = f . x2 ; :: thesis:

now :: thesis:

per cases by A2, A4, FINSEQ_1:2, TARSKI:def 2;

case ( x1 = 1 & x2 = 1 ) ; :: thesis:

hence x1 = x2 ; :: thesis:

end;

case A6: ( x1 = 1 & x2 = 2 ) ; :: thesis:

then f . x1 = 1 by A3, FINSEQ_1:44;
hence contradiction by A3, A5, A6, FINSEQ_1:44; :: thesis:

end;

case A7: ( x1 = 2 & x2 = 1 ) ; :: thesis:

then f . x1 = 2 by A3, FINSEQ_1:44;
hence contradiction by A3, A5, A7, FINSEQ_1:44; :: thesis:

end;

case ( x1 = 2 & x2 = 2 ) ; :: thesis:

hence x1 = x2 ; :: thesis:

end;

end;

end;

hence x1 = x2 ; :: thesis:

end;

then A8: f is one-to-one by FUNCT_1:def 4;

now :: thesis:

let x be object ; :: thesis:
assume x in rng f ; :: thesis:
then consider z being object such that
A9: z in dom f and
A10: f . z = x by FUNCT_1:def 3;
len f = 2 by A3, FINSEQ_1:44;
then dom f = Seg 2 by FINSEQ_1:def 3;
then ( z = 1 or z = 2 ) by A9, FINSEQ_1:2, TARSKI:def 2;
then ( x = 1 or x = 2 ) by A3, A10, FINSEQ_1:44;
hence x in Seg 2 ; :: thesis:

end;

then A11: rng f c= Seg 2 ;
Seg 2 c= rng f

proof

let z be object ; :: according to TARSKI:def 3 :: thesis:
assume z in Seg 2 ; :: thesis:
then ( z = 1 or z = 2 ) by FINSEQ_1:2, TARSKI:def 2;
then A12: ( z = f . 1 or z = f . 2 ) by A3, FINSEQ_1:44;
( 1 in dom f & 2 in dom f ) by A2;
hence z in rng f by A12, FUNCT_1:def 3; :: thesis:

end;

then rng f = Seg 2 by A11;
then g is onto by FUNCT_2:def 3;
hence f is Permutation of (Seg 2) by A8; :: thesis:

end;

case A13: f = <*2,1*> ; :: thesis:

for x1, x2 being object st x1 in dom f & x2 in dom f & f . x1 = f . x2 holds
x1 = x2

proof

let x1, x2 be object ; :: thesis:
assume that
A14: ( x1 in dom f & x2 in dom f ) and
A15: f . x1 = f . x2 ; :: thesis:

now :: thesis:

per cases by A2, A14, FINSEQ_1:2, TARSKI:def 2;

case ( x1 = 1 & x2 = 1 ) ; :: thesis:

hence x1 = x2 ; :: thesis:

end;

case A16: ( x1 = 1 & x2 = 2 ) ; :: thesis:

then f . x1 = 2 by A13, FINSEQ_1:44;
hence contradiction by A13, A15, A16, FINSEQ_1:44; :: thesis:

end;

case A17: ( x1 = 2 & x2 = 1 ) ; :: thesis:

then f . x1 = 1 by A13, FINSEQ_1:44;
hence contradiction by A13, A15, A17, FINSEQ_1:44; :: thesis:

end;

case ( x1 = 2 & x2 = 2 ) ; :: thesis:

hence x1 = x2 ; :: thesis:

end;

end;

end;

hence x1 = x2 ; :: thesis:

end;

then A18: f is one-to-one by FUNCT_1:def 4;

now :: thesis:

let x be object ; :: thesis:
assume x in rng f ; :: thesis:
then consider z being object such that
A19: z in dom f and
A20: f . z = x by FUNCT_1:def 3;
len f = 2 by A13, FINSEQ_1:44;
then dom f = Seg 2 by FINSEQ_1:def 3;
then ( z = 1 or z = 2 ) by A19, FINSEQ_1:2, TARSKI:def 2;
then ( x = 2 or x = 1 ) by A13, A20, FINSEQ_1:44;
hence x in Seg 2 ; :: thesis:

end;

then A21: rng f c= Seg 2 ;
Seg 2 c= rng f

proof

let z be object ; :: according to TARSKI:def 3 :: thesis:
assume z in Seg 2 ; :: thesis:
then ( z = 1 or z = 2 ) by FINSEQ_1:2, TARSKI:def 2;
then A22: ( z = f . 2 or z = f . 1 ) by A13, FINSEQ_1:44;
( 2 in dom f & 1 in dom f ) by A2;
hence z in rng f by A22, FUNCT_1:def 3; :: thesis:

end;

then rng f = Seg 2 by A21;
then g is onto by FUNCT_2:def 3;
hence f is Permutation of (Seg 2) by A18; :: thesis:

end;

end;

end;

hence f is Permutation of (Seg 2) ; :: thesis: