let n be Nat; :: thesis:
let K be commutative Ring; :: 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:
2Set (Seg (n + 2)) in Fin (2Set (Seg (n + 2))) by FINSUB_1:def 5;
then In ((2Set (Seg (n + 2))),(Fin (2Set (Seg (n + 2))))) = 2Set (Seg (n + 2)) by SUBSET_1:def 8;
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₁[ object , object ] means ex D1 being set st
( D1 = $1 & ( for k being Nat st k in D1 & 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 object ; :: 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 object ; :: 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 object ; :: 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 object ; :: 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;
A17: D1 /\ D2 c= {{i,j}}

proof

let x be object ; :: 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_1:def 12;
then A22: dom q = Seg (n + 2) by FUNCT_2:52;
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 object st x in D1 holds
ex y being object st
( y in D2 & S₁[x,y] )

proof

let x be object ; :: 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 :: thesis:

per cases ;

suppose A35: j9 = j ; :: thesis:

take X = {i,j}; :: thesis:
thus X in D2 by A26, A24, A9; :: thesis:
reconsider xx = x as set by TARSKI:1;
take xx = xx; :: thesis:
thus xx = x ; :: thesis:
let k be Nat; :: thesis:
assume that
A36: k in xx 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:
reconsider xx = x as set by TARSKI:1;
take xx = xx; :: thesis:
thus xx = x ; :: thesis:
let k be Nat; :: thesis:
assume that
A40: k in xx 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 object st
( y in D2 & S₁[x,y] ) ; :: thesis:

end;

consider f being Function of D1,D2 such that
A42: for x being object 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 object st y in D2 holds
ex x being object st
( x in D1 & y = f . x )

proof

let y be object ; :: 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 :: thesis:

per cases ;

suppose A51: i1 = i ; :: thesis:

A52: {i,j} in D1 by A25, A24, A9;
then S₁[s,f . s] by A42, A50, A51;
then f . s = y by A5, A26, A45, A50, A51;
hence ex x being object 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;
A57: i1 in {i,i1} by TARSKI:def 2;
S₁[{i,i1},f . {i,i1}] by A42, A56;
then f . {i,i1} = {j,i1} by A49, A53, A57;
hence ex x being object st
( x in D1 & y = f . x ) by A45, A50, A56; :: thesis:

end;

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

end;

then A58: rng f = D2 by FUNCT_2:10;
for x1, x2 being object st x1 in D1 & x2 in D1 & f . x1 = f . x2 holds
x1 = x2

proof

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

now :: thesis:

per cases ;

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

hence x1 = x2 by A62, A65, A66, A69; :: thesis:

end;

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

S₁[x2,f . x2] by A42, A60;
then A73: f . x2 = {i,j} by A66, A68, A70, A72;
S₁[x1,f . x1] by A42, A59;
then f . x1 = {j,j1} by A62, A64, A71, A72;
hence x1 = x2 by A5, A61, A64, A67, A69, A72, A73, TARSKI:def 2; :: thesis:

end;

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

S₁[x2,f . x2] by A42, A60;
then A75: f . x2 = {j,j2} by A66, A68, A70, A74;
S₁[x1,f . x1] by A42, A59;
then f . x1 = {i,j} by A62, A64, A71, A74;
hence x1 = x2 by A5, A61, A63, A65, A68, A74, A75, TARSKI:def 2; :: thesis:

end;

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

S₁[x2,f . x2] by A42, A60;
then A77: f . x2 = {j,j2} by A66, A68, A70, A76;
A78: j1 in {j,j1} by TARSKI:def 2;
S₁[x1,f . x1] by A42, A59;
then f . x1 = {j,j1} by A62, A64, A71, A76;
hence x1 = x2 by A61, A62, A65, A66, A69, A76, A77, A78, TARSKI:def 2; :: thesis:

end;

hence x1 = x2 ; :: thesis:

end;

then f is one-to-one by A43, FUNCT_2:19;
then D1,D2 are_equipotent by A58, A44, WELLORD2:def 4;
then A79: card D1 = card D2 by CARD_1:5;
{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:31;
then D1 /\ D2 = {{i,j}} by A17;
then card D = ((card D1) + (card D1)) - (card {{i,j}}) by A79, A16, CARD_2:45
.= ((c1 + 1) + (c1 + 1)) - 1 by CARD_1:30
.= (2 * c1) + 1 ;
then (card D) mod 2 = 1 mod 2 by NAT_D:21;
hence sgn (pq,K) = - (sgn (p,K)) by 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
A80: i <> j and
A81: q . i = j and
A82: q . j = i and
for k being Nat st k <> i & k <> j & k in dom q holds
q . k = k by A2;
( i < j or j < i ) by A80, XXREAL_0:1;
hence sgn (pq,K) = - (sgn (p,K)) by A4, A81, A82; :: thesis: