let f be FinSequence; :: thesis: ( ( f = <*1,2*> or f = <*2,1*> ) implies f is Permutation of (Seg 2) )
assume A1: ( f = <*1,2*> or f = <*2,1*> ) ; :: thesis: f is Permutation of (Seg 2)
( 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: ( not y in rng f or y in Seg 2 )
assume y in rng f ; :: thesis: y in Seg 2
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;
hence y in Seg 2 ; :: thesis: verum

end;

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

now :: thesis: ( ( f = <*1,2*> & f is Permutation of (Seg 2) ) or ( f = <*2,1*> & f is Permutation of (Seg 2) ) )

per cases ( f = <*1,2*> or f = <*2,1*> ) by A1;

case A3: f = <*1,2*> ; :: thesis: f is Permutation of (Seg 2)

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: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 implies x1 = x2 )
assume that
A4: ( x1 in dom f & x2 in dom f ) and
A5: f . x1 = f . x2 ; :: thesis: x1 = x2

now :: thesis: ( ( x1 = 1 & x2 = 1 & x1 = x2 ) or ( x1 = 1 & x2 = 2 & contradiction ) or ( x1 = 2 & x2 = 1 & contradiction ) or ( x1 = 2 & x2 = 2 & x1 = x2 ) )

per cases ( ( x1 = 1 & x2 = 1 ) or ( x1 = 1 & x2 = 2 ) or ( x1 = 2 & x2 = 1 ) or ( x1 = 2 & x2 = 2 ) ) by A2, A4, FINSEQ_1:2, TARSKI:def 2;

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

hence x1 = x2 ; :: thesis: verum

end;

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

thus contradiction by A3, A5, A6; :: thesis: verum

end;

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

thus contradiction by A3, A5, A7; :: thesis: verum

end;

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

hence x1 = x2 ; :: thesis: verum

end;

end;

end;

hence x1 = x2 ; :: thesis: verum

end;

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

now :: thesis: for x being object st x in rng f holds
x in Seg 2

let x be object ; :: thesis: ( x in rng f implies x in Seg 2 )
assume x in rng f ; :: thesis: x in Seg 2
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;
hence x in Seg 2 ; :: thesis: verum

end;

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

proof

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

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: verum

end;

case A13: f = <*2,1*> ; :: thesis: f is Permutation of (Seg 2)

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: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 implies x1 = x2 )
assume that
A14: ( x1 in dom f & x2 in dom f ) and
A15: f . x1 = f . x2 ; :: thesis: x1 = x2

now :: thesis: ( ( x1 = 1 & x2 = 1 & x1 = x2 ) or ( x1 = 1 & x2 = 2 & contradiction ) or ( x1 = 2 & x2 = 1 & contradiction ) or ( x1 = 2 & x2 = 2 & x1 = x2 ) )

per cases ( ( x1 = 1 & x2 = 1 ) or ( x1 = 1 & x2 = 2 ) or ( x1 = 2 & x2 = 1 ) or ( x1 = 2 & x2 = 2 ) ) by A2, A14, FINSEQ_1:2, TARSKI:def 2;

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

hence x1 = x2 ; :: thesis: verum

end;

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

thus contradiction by A13, A15, A16; :: thesis: verum

end;

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

thus contradiction by A13, A15, A17; :: thesis: verum

end;

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

hence x1 = x2 ; :: thesis: verum

end;

end;

end;

hence x1 = x2 ; :: thesis: verum

end;

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

now :: thesis: for x being object st x in rng f holds
x in Seg 2

let x be object ; :: thesis: ( x in rng f implies x in Seg 2 )
assume x in rng f ; :: thesis: x in Seg 2
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;
hence x in Seg 2 ; :: thesis: verum

end;

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

proof

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

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: verum

end;

end;

end;

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