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)
A2: len <*1,2*> = 2 by FINSEQ_1:61;
len <*2,1*> = 2 by FINSEQ_1:61;
then A3: dom f = Seg 2 by A1, A2, FINSEQ_1:def 3;
rng f c= Seg 2
proof
let y be set ; :: 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 consider x being set such that
A4: ( x in dom f & y = f . x ) by FUNCT_1:def 5;
( y = f . 1 or y = f . 2 ) by A3, A4, FINSEQ_1:4, TARSKI:def 2;
then ( y = 1 or y = 2 or y = 2 or y = 1 ) by A1, FINSEQ_1:61;
hence y in Seg 2 ; :: thesis: verum
end;
then reconsider g = f as Function of (Seg 2),(Seg 2) by A3, FUNCT_2:4;
now
per cases ( f = <*1,2*> or f = <*2,1*> ) by A1;
case A5: f = <*1,2*> ; :: thesis: f is Permutation of (Seg 2)
for x1, x2 being set st x1 in dom f & x2 in dom f & f . x1 = f . x2 holds
x1 = x2
proof
let x1, x2 be set ; :: thesis: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 implies x1 = x2 )
assume A6: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 ) ; :: thesis: x1 = x2
now
per cases ( ( x1 = 1 & x2 = 1 ) or ( x1 = 1 & x2 = 2 ) or ( x1 = 2 & x2 = 1 ) or ( x1 = 2 & x2 = 2 ) ) by A3, A6, FINSEQ_1:4, TARSKI:def 2;
case ( x1 = 1 & x2 = 1 ) ; :: thesis: x1 = x2
hence x1 = x2 ; :: 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 A9: f is one-to-one by FUNCT_1:def 8;
rng f = Seg 2
proof
now
let x be set ; :: thesis: ( x in rng f implies x in Seg 2 )
assume x in rng f ; :: thesis: x in Seg 2
then consider z being set such that
A11: ( z in dom f & f . z = x ) by FUNCT_1:def 5;
len f = 2 by A5, FINSEQ_1:61;
then dom f = Seg 2 by FINSEQ_1:def 3;
then ( z = 1 or z = 2 ) by A11, FINSEQ_1:4, TARSKI:def 2;
then ( x = 1 or x = 2 ) by A5, A11, FINSEQ_1:61;
hence x in Seg 2 ; :: thesis: verum
end;
then A12: rng f c= Seg 2 by TARSKI:def 3;
Seg 2 c= rng f
proof
let z be set ; :: 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:4, TARSKI:def 2;
then A13: ( z = f . 1 or z = f . 2 ) by A5, FINSEQ_1:61;
A14: 1 in dom f by A3;
2 in dom f by A3;
hence z in rng f by A13, A14, FUNCT_1:def 5; :: thesis: verum
end;
hence rng f = Seg 2 by A12, XBOOLE_0:def 10; :: thesis: verum
end;
then g is onto by FUNCT_2:def 3;
hence f is Permutation of (Seg 2) by A9; :: thesis: verum
end;
case A15: f = <*2,1*> ; :: thesis: f is Permutation of (Seg 2)
for x1, x2 being set st x1 in dom f & x2 in dom f & f . x1 = f . x2 holds
x1 = x2
proof
let x1, x2 be set ; :: thesis: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 implies x1 = x2 )
assume A16: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 ) ; :: thesis: x1 = x2
now
per cases ( ( x1 = 1 & x2 = 1 ) or ( x1 = 1 & x2 = 2 ) or ( x1 = 2 & x2 = 1 ) or ( x1 = 2 & x2 = 2 ) ) by A3, A16, FINSEQ_1:4, TARSKI:def 2;
case ( x1 = 1 & x2 = 1 ) ; :: thesis: x1 = x2
hence x1 = x2 ; :: 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 A19: f is one-to-one by FUNCT_1:def 8;
rng f = Seg 2
proof
now
let x be set ; :: thesis: ( x in rng f implies x in Seg 2 )
assume x in rng f ; :: thesis: x in Seg 2
then consider z being set such that
A21: ( z in dom f & f . z = x ) by FUNCT_1:def 5;
len f = 2 by A15, FINSEQ_1:61;
then dom f = Seg 2 by FINSEQ_1:def 3;
then ( z = 1 or z = 2 ) by A21, FINSEQ_1:4, TARSKI:def 2;
then ( x = 2 or x = 1 ) by A15, A21, FINSEQ_1:61;
hence x in Seg 2 ; :: thesis: verum
end;
then A22: rng f c= Seg 2 by TARSKI:def 3;
Seg 2 c= rng f
proof
let z be set ; :: 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:4, TARSKI:def 2;
then A23: ( z = f . 2 or z = f . 1 ) by A15, FINSEQ_1:61;
A24: 2 in dom f by A3;
1 in dom f by A3;
hence z in rng f by A23, A24, FUNCT_1:def 5; :: thesis: verum
end;
hence rng f = Seg 2 by A22, XBOOLE_0:def 10; :: thesis: verum
end;
then g is onto by FUNCT_2:def 3;
hence f is Permutation of (Seg 2) by A19; :: thesis: verum
end;
end;
end;
hence f is Permutation of (Seg 2) ; :: thesis: verum