let n be Nat; :: thesis:
let K be Field; :: thesis:
set n2 = n + 2;
set 2SS = 2Set (Seg (n + 2));
let p, q, pq be Element of Permutations (n + 2); :: thesis:
assume that
A1: pq = p * q and
A2: q is being_transposition ; :: thesis:
A3: FinOmega (2Set (Seg (n + 2))) = 2Set (Seg (n + 2)) by MATRIX_2:def 17;
then reconsider 2S = 2Set (Seg (n + 2)) as Element of Fin (2Set (Seg (n + 2))) ;
A4: for i, j being Nat st i < j & q . i = j holds
sgn pq,K = - (sgn p,K)

let i, j be Nat; :: thesis:
assume that
A5: i < j and
A6: q . i = j ; :: thesis:

per cases ;

suppose A7: 1_ K = - (1_ K) ; :: thesis:

then sgn pq,K = - (1_ K) by Th11;
hence sgn pq,K = - (sgn p,K) by A7, Th11; :: thesis:

end;

suppose A8: 1_ K <> - (1_ K) ; :: thesis:

set P2 = Part_sgn p,K;
set P1 = Part_sgn pq,K;
A9: (Part_sgn pq,K) . {i,j} <> (Part_sgn p,K) . {i,j} by A1, A2, A5, A6, A8, Th10;
defpred S₁[ set , set ] means for k being Nat st k in $1 & k <> i holds
( ( k <> j implies $2 = {j,k} ) & ( k = j implies $2 = {i,j} ) );
set D = { s where s is Element of 2Set (Seg (n + 2)) : ( s in 2S & (Part_sgn pq,K) . s <> (Part_sgn p,K) . s ) } ;
{ s where s is Element of 2Set (Seg (n + 2)) : ( s in 2S & (Part_sgn pq,K) . s <> (Part_sgn p,K) . s ) } c= 2S

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in { s where s is Element of 2Set (Seg (n + 2)) : ( s in 2S & (Part_sgn pq,K) . s <> (Part_sgn p,K) . s ) } ; :: thesis:
then ex s being Element of 2Set (Seg (n + 2)) st
( x = s & s in 2S & (Part_sgn pq,K) . s <> (Part_sgn p,K) . s ) ;
hence x in 2S ; :: thesis:

end;

then reconsider D = { s where s is Element of 2Set (Seg (n + 2)) : ( s in 2S & (Part_sgn pq,K) . s <> (Part_sgn p,K) . s ) } as finite set ;
set D1 = { s where s is Element of 2Set (Seg (n + 2)) : ( s in 2S & (Part_sgn pq,K) . s <> (Part_sgn p,K) . s & i in s ) } ;
set D2 = { s where s is Element of 2Set (Seg (n + 2)) : ( s in 2S & (Part_sgn pq,K) . s <> (Part_sgn p,K) . s & j in s ) } ;
A10: { s where s is Element of 2Set (Seg (n + 2)) : ( s in 2S & (Part_sgn pq,K) . s <> (Part_sgn p,K) . s & i in s ) } c= D

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in { s where s is Element of 2Set (Seg (n + 2)) : ( s in 2S & (Part_sgn pq,K) . s <> (Part_sgn p,K) . s & i in s ) } ; :: thesis:
then ex s being Element of 2Set (Seg (n + 2)) st
( x = s & s in 2S & (Part_sgn pq,K) . s <> (Part_sgn p,K) . s & i in s ) ;
hence x in D ; :: thesis:

end;

A11: { s where s is Element of 2Set (Seg (n + 2)) : ( s in 2S & (Part_sgn pq,K) . s <> (Part_sgn p,K) . s & j in s ) } c= D

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in { s where s is Element of 2Set (Seg (n + 2)) : ( s in 2S & (Part_sgn pq,K) . s <> (Part_sgn p,K) . s & j in s ) } ; :: thesis:
then ex s being Element of 2Set (Seg (n + 2)) st
( x = s & s in 2S & (Part_sgn pq,K) . s <> (Part_sgn p,K) . s & j in s ) ;
hence x in D ; :: thesis:

end;

then reconsider D1 = { s where s is Element of 2Set (Seg (n + 2)) : ( s in 2S & (Part_sgn pq,K) . s <> (Part_sgn p,K) . s & i in s ) } , D2 = { s where s is Element of 2Set (Seg (n + 2)) : ( s in 2S & (Part_sgn pq,K) . s <> (Part_sgn p,K) . s & j in s ) } as finite set by A10;
A12: j in dom q by A2, A5, A6, Th8;
A13: D c= D1 \/ D2

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in D ; :: thesis:
then consider s being Element of 2Set (Seg (n + 2)) such that
A14: x = s and
s in 2S and
A15: (Part_sgn pq,K) . s <> (Part_sgn p,K) . s ;
( i in s or j in s ) by A1, A2, A5, A6, A15, Th9;
then ( x in D1 or x in D2 ) by A14, A15;
hence x in D1 \/ D2 by XBOOLE_0:def 3; :: thesis:

end;

D1 \/ D2 c= D by A10, A11, XBOOLE_1:8;
then A16: D1 \/ D2 = D by A13, XBOOLE_0:def 10;
A17: D1 /\ D2 c= {{i,j}}

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume A18: x in D1 /\ D2 ; :: thesis:
then x in D1 by XBOOLE_0:def 4;
then A19: ex s1 being Element of 2Set (Seg (n + 2)) st
( x = s1 & s1 in 2S & (Part_sgn pq,K) . s1 <> (Part_sgn p,K) . s1 & i in s1 ) ;
then consider i9, j9 being Nat such that
i9 in Seg (n + 2) and
j9 in Seg (n + 2) and
i9 < j9 and
A20: {i9,j9} = x by Th1;
x in D2 by A18, XBOOLE_0:def 4;
then ex s2 being Element of 2Set (Seg (n + 2)) st
( x = s2 & s2 in 2S & (Part_sgn pq,K) . s2 <> (Part_sgn p,K) . s2 & j in s2 ) ;
then A21: ( j = i9 or j = j9 ) by A20, TARSKI:def 2;
( i = i9 or i = j9 ) by A19, A20, TARSKI:def 2;
hence x in {{i,j}} by A5, A20, A21, TARSKI:def 1; :: thesis:

end;

q is Permutation of (Seg (n + 2)) by MATRIX_2:def 11;
then A22: dom q = Seg (n + 2) by FUNCT_2:67;
A23: i in dom q by A2, A5, A6, Th8;
then A24: {i,j} in 2S by A5, A12, A22, Th1;
A25: i in {i,j} by TARSKI:def 2;
then {i,j} in D1 by A24, A9;
then card D1 > 0 ;
then reconsider c1 = (card D1) - 1 as Nat by NAT_1:20;
A26: j in {i,j} by TARSKI:def 2;
then A27: {i,j} in D2 by A24, A9;
A28: for x being set st x in D1 holds
ex y being set st
( y in D2 & S₁[x,y] )

proof

let x be set ; :: thesis:
assume x in D1 ; :: thesis:
then consider s being Element of 2Set (Seg (n + 2)) such that
A29: x = s and
s in 2S and
A30: (Part_sgn pq,K) . s <> (Part_sgn p,K) . s and
A31: i in s ;
consider j9 being Nat such that
A32: j9 in Seg (n + 2) and
A33: j9 <> i and
A34: s = {i,j9} by A31, Lm2;

now

per cases ;

suppose A35: j9 = j ; :: thesis:

take X = {i,j}; :: thesis:
thus X in D2 by A26, A24, A9; :: thesis:
let k be Nat; :: thesis:
assume that
A36: k in x and
k <> i ; :: thesis:
thus ( ( k <> j implies X = {j,k} ) & ( k = j implies X = {i,j} ) ) by A29, A34, A35, A36, TARSKI:def 2; :: thesis:

end;

suppose A37: j9 <> j ; :: thesis:

take X = {j,j9}; :: thesis:
( j < j9 or j > j9 ) by A37, XXREAL_0:1;
then A38: X in 2Set (Seg (n + 2)) by A12, A22, A32, Th1;
A39: j in X by TARSKI:def 2;
(Part_sgn pq,K) . X <> (Part_sgn p,K) . X by A1, A2, A5, A6, A8, A30, A32, A33, A34, A37, Th10;
hence X in D2 by A39, A38; :: thesis:
let k be Nat; :: thesis:
assume that
A40: k in x and
A41: k <> i ; :: thesis:
thus ( ( k <> j implies X = {j,k} ) & ( k = j implies X = {i,j} ) ) by A29, A34, A37, A40, A41, TARSKI:def 2; :: thesis:

end;

hence ex y being set st
( y in D2 & S₁[x,y] ) ; :: thesis:

end;

consider f being Function of D1,D2 such that
A42: for x being set st x in D1 holds
S₁[x,f . x] from FUNCT_2:sch 1(A28);
A43: {i,j} in D2 by A26, A24, A9;
then A44: dom f = D1 by FUNCT_2:def 1;
for y being set st y in D2 holds
ex x being set st
( x in D1 & y = f . x )

proof

let y be set ; :: thesis:
assume y in D2 ; :: thesis:
then consider s being Element of 2Set (Seg (n + 2)) such that
A45: s = y and
s in 2S and
A46: (Part_sgn pq,K) . s <> (Part_sgn p,K) . s and
A47: j in s ;
consider i1 being Nat such that
A48: i1 in Seg (n + 2) and
A49: i1 <> j and
A50: s = {j,i1} by A47, Lm2;

now

per cases ;

suppose A51: i1 = i ; :: thesis:

A52: {i,j} in D1 by A25, A24, A9;
then f . s = y by A5, A26, A42, A45, A50, A51;
hence ex x being set st
( x in D1 & y = f . x ) by A50, A51, A52; :: thesis:

end;

suppose A53: i1 <> i ; :: thesis:

then ( i < i1 or i > i1 ) by XXREAL_0:1;
then A54: {i,i1} in 2Set (Seg (n + 2)) by A23, A22, A48, Th1;
A55: i in {i,i1} by TARSKI:def 2;
(Part_sgn pq,K) . {i,i1} <> (Part_sgn p,K) . {i,i1} by A1, A2, A5, A6, A8, A46, A48, A49, A50, A53, Th10;
then A56: {i,i1} in D1 by A54, A55;
i1 in {i,i1} by TARSKI:def 2;
then f . {i,i1} = {j,i1} by A42, A49, A53, A56;
hence ex x being set st
( x in D1 & y = f . x ) by A45, A50, A56; :: thesis:

end;

hence ex x being set st
( x in D1 & y = f . x ) ; :: thesis:

end;

then A57: rng f = D2 by A43, FUNCT_2:16;
for x1, x2 being set st x1 in D1 & x2 in D1 & f . x1 = f . x2 holds
x1 = x2

proof

let x1, x2 be set ; :: thesis:
assume that
A58: x1 in D1 and
A59: x2 in D1 and
A60: f . x1 = f . x2 ; :: thesis:
consider s1 being Element of 2Set (Seg (n + 2)) such that
A61: x1 = s1 and
s1 in 2S and
(Part_sgn pq,K) . s1 <> (Part_sgn p,K) . s1 and
A62: i in s1 by A58;
consider j1 being Nat such that
j1 in Seg (n + 2) and
A63: i <> j1 and
A64: {i,j1} = s1 by A62, Lm2;
consider s2 being Element of 2Set (Seg (n + 2)) such that
A65: x2 = s2 and
s2 in 2S and
(Part_sgn pq,K) . s2 <> (Part_sgn p,K) . s2 and
A66: i in s2 by A59;
consider j2 being Nat such that
j2 in Seg (n + 2) and
A67: i <> j2 and
A68: {i,j2} = s2 by A66, Lm2;
A69: j2 in s2 by A68, TARSKI:def 2;
A70: j1 in s1 by A64, TARSKI:def 2;

now

per cases ;

case ( j = j1 & j = j2 ) ; :: thesis:

hence x1 = x2 by A61, A64, A65, A68; :: thesis:

end;

case A71: ( j <> j1 & j = j2 ) ; :: thesis:

then A72: f . x2 = {i,j} by A42, A59, A65, A67, A69;
f . x1 = {j,j1} by A42, A58, A61, A63, A70, A71;
hence x1 = x2 by A5, A60, A63, A66, A68, A71, A72, TARSKI:def 2; :: thesis:

end;

case A73: ( j = j1 & j <> j2 ) ; :: thesis:

then A74: f . x2 = {j,j2} by A42, A59, A65, A67, A69;
f . x1 = {i,j} by A42, A58, A61, A63, A70, A73;
hence x1 = x2 by A5, A60, A62, A64, A67, A73, A74, TARSKI:def 2; :: thesis:

end;

case A75: ( j <> j1 & j <> j2 ) ; :: thesis:

then A76: f . x2 = {j,j2} by A42, A59, A65, A67, A69;
A77: j1 in {j,j1} by TARSKI:def 2;
f . x1 = {j,j1} by A42, A58, A61, A63, A70, A75;
hence x1 = x2 by A60, A61, A64, A65, A68, A75, A76, A77, TARSKI:def 2; :: thesis:

end;

hence x1 = x2 ; :: thesis:

end;

then f is one-to-one by A43, FUNCT_2:25;
then D1,D2 are_equipotent by A57, A44, WELLORD2:def 4;
then A78: card D1 = card D2 by CARD_1:21;
{i,j} in D1 by A25, A24, A9;
then {i,j} in D1 /\ D2 by A27, XBOOLE_0:def 4;
then {{i,j}} c= D1 /\ D2 by ZFMISC_1:37;
then D1 /\ D2 = {{i,j}} by A17, XBOOLE_0:def 10;
then card D = ((card D1) + (card D1)) - (card {{i,j}}) by A78, A16, CARD_2:64
.= ((c1 + 1) + (c1 + 1)) - 1 by CARD_1:50
.= (2 * c1) + 1 ;
then (card D) mod 2 = 1 mod 2 by NAT_D:21;
hence sgn pq,K = - (sgn p,K) by A3, Th7, NAT_D:14; :: thesis:

end;

hence sgn pq,K = - (sgn p,K) ; :: thesis:

end;

consider i, j being Nat such that
i in dom q and
j in dom q and
A79: i <> j and
A80: q . i = j and
A81: q . j = i and
for k being Nat st k <> i & k <> j & k in dom q holds
q . k = k by A2, MATRIX_2:def 14;
( i < j or j < i ) by A79, XXREAL_0:1;
hence sgn pq,K = - (sgn p,K) by A4, A80, A81; :: thesis: