let n be Nat; :: thesis:
let K be Fanoian Field; :: thesis:
let p2 be Element of Permutations (n + 2); :: thesis:
let i, j be Nat; :: thesis:
assume that
A1: i in Seg (n + 2) and
A2: p2 . i = j ; :: thesis:
reconsider N = n as Element of NAT by ORDINAL1:def 12;
set n2 = N + 2;
reconsider p29 = p2 as Permutation of (finSeg (N + 2)) by MATRIX_1:def 12;
A3: rng p29 = Seg (N + 2) by FUNCT_2:def 3;
1 <= i by A1, FINSEQ_1:1;
then reconsider i1 = i - 1 as Element of NAT by NAT_1:21;
deffunc H₁( object ) -> set = {$1,i};
set Ui = (finSeg (N + 2)) \ (Seg i);
set Li = finSeg i1;
set SS = 2Set (Seg (n + 2));
set X = { {k,i} where k is Nat : {k,i} in 2Set (Seg (n + 2)) } ;
A4: { {k,i} where k is Nat : {k,i} in 2Set (Seg (n + 2)) } c= 2Set (Seg (n + 2))

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in { {k,i} where k is Nat : {k,i} in 2Set (Seg (n + 2)) } ; :: thesis:
then ex k being Nat st
( x = {k,i} & {k,i} in 2Set (Seg (N + 2)) ) ;
hence x in 2Set (Seg (n + 2)) ; :: thesis:

end;

then reconsider X = { {k,i} where k is Nat : {k,i} in 2Set (Seg (n + 2)) } as Element of Fin (2Set (Seg (n + 2))) by FINSUB_1:def 5;
set Y = { s where s is Element of 2Set (Seg (n + 2)) : ( s in X & (Part_sgn (p2,K)) . s = - (1_ K) ) } ;
A5: { s where s is Element of 2Set (Seg (n + 2)) : ( s in X & (Part_sgn (p2,K)) . s = - (1_ K) ) } c= X

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 X & (Part_sgn (p2,K)) . s = - (1_ K) ) } ; :: thesis:
then ex s being Element of 2Set (Seg (n + 2)) st
( s = x & s in X & (Part_sgn (p2,K)) . s = - (1_ K) ) ;
hence x in X ; :: thesis:

end;

then A6: { s where s is Element of 2Set (Seg (n + 2)) : ( s in X & (Part_sgn (p2,K)) . s = - (1_ K) ) } c= 2Set (Seg (n + 2)) by A4;
dom p29 = Seg (N + 2) by FUNCT_2:52;
then A7: p2 . i in rng p2 by A1, FUNCT_1:def 3;
then 1 <= j by A2, A3, FINSEQ_1:1;
then reconsider j1 = j - 1 as Element of NAT by NAT_1:21;
reconsider Y = { s where s is Element of 2Set (Seg (n + 2)) : ( s in X & (Part_sgn (p2,K)) . s = - (1_ K) ) } as Element of Fin (2Set (Seg (n + 2))) by A6, FINSUB_1:def 5;
consider f being Function such that
A8: ( dom f = (finSeg i1) \/ ((finSeg (N + 2)) \ (Seg i)) & ( for x being object st x in (finSeg i1) \/ ((finSeg (N + 2)) \ (Seg i)) holds
f . x = H₁(x) ) ) from FUNCT_1:sch 3();
A9: f " Y c= dom f by RELAT_1:132;
then reconsider fY = f " Y as finite set by A8;
A10: (finSeg i1) \/ ((finSeg (N + 2)) \ (Seg i)) c= (Seg (N + 2)) \ {i}

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A11: x in (finSeg i1) \/ ((finSeg (N + 2)) \ (Seg i)) ; :: thesis:

per cases by A11, XBOOLE_0:def 3;

suppose A12: x in finSeg i1 ; :: thesis:

A13: i <= N + 2 by A1, FINSEQ_1:1;
consider k being Nat such that
A14: x = k and
A15: 1 <= k and
A16: k <= i1 by A12;
A17: i1 < i1 + 1 by NAT_1:13;
then k < i by A16, XXREAL_0:2;
then k <= N + 2 by A13, XXREAL_0:2;
then A18: k in Seg (N + 2) by A15;
not k in {i} by A16, A17, TARSKI:def 1;
hence x in (Seg (N + 2)) \ {i} by A14, A18, XBOOLE_0:def 5; :: thesis:

end;

suppose A19: x in (finSeg (N + 2)) \ (Seg i) ; :: thesis:

A20: i1 + 1 in Seg i by FINSEQ_1:4;
not x in Seg i by A19, XBOOLE_0:def 5;
then not x in {i} by A20, TARSKI:def 1;
hence x in (Seg (N + 2)) \ {i} by A19, XBOOLE_0:def 5; :: thesis:

end;

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
A21: x1 in dom f and
A22: x2 in dom f and
A23: f . x1 = f . x2 ; :: thesis:
A24: f . x2 = H₁(x2) by A8, A22;
not x1 in {i} by A10, A8, A21, XBOOLE_0:def 5;
then A25: x1 <> i by TARSKI:def 1;
f . x1 = H₁(x1) by A8, A21;
then x1 in {i,x2} by A23, A24, TARSKI:def 2;
hence x1 = x2 by A25, TARSKI:def 2; :: thesis:

end;

then f is one-to-one by FUNCT_1:def 4;
then f .: fY,fY are_equipotent by A9, CARD_1:33;
then A26: card (f .: fY) = card fY by CARD_1:5;
(finSeg (N + 2)) \ {i} c= (finSeg i1) \/ ((finSeg (N + 2)) \ (Seg i))

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A27: x in (finSeg (N + 2)) \ {i} ; :: thesis:
x in finSeg (N + 2) by A27;
then consider k being Nat such that
A28: x = k and
A29: 1 <= k and
A30: k <= N + 2 ;
not k in {i} by A27, A28, XBOOLE_0:def 5;
then A31: k <> i by TARSKI:def 1;

per cases by A31, XXREAL_0:1;

suppose k < i1 + 1 ; :: thesis:

then k <= i1 by NAT_1:13;
then x in finSeg i1 by A28, A29;
hence x in (finSeg i1) \/ ((finSeg (N + 2)) \ (Seg i)) by XBOOLE_0:def 3; :: thesis:

end;

suppose k > i1 + 1 ; :: thesis:

then A32: not x in Seg i by A28, FINSEQ_1:1;
x in Seg (N + 2) by A28, A29, A30;
then x in (finSeg (N + 2)) \ (Seg i) by A32, XBOOLE_0:def 5;
hence x in (finSeg i1) \/ ((finSeg (N + 2)) \ (Seg i)) by XBOOLE_0:def 3; :: thesis:

end;

then A33: (finSeg (N + 2)) \ {i} = (finSeg i1) \/ ((finSeg (N + 2)) \ (Seg i)) by A10, XBOOLE_0:def 10;
A34: rng f c= X

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in rng f ; :: thesis:
then consider y being object such that
A35: y in dom f and
A36: f . y = x by FUNCT_1:def 3;
y in finSeg (N + 2) by A33, A8, A35;
then consider k being Nat such that
A37: k = y and
A38: 1 <= k and
A39: k <= N + 2 ;
A40: f . k = {i,k} by A8, A35, A37;
not y in {i} by A10, A8, A35, XBOOLE_0:def 5;
then i <> k by A37, TARSKI:def 1;
then A41: ( k < i or i < k ) by XXREAL_0:1;
k in Seg (N + 2) by A38, A39;
then {i,k} in 2Set (Seg (n + 2)) by A1, A41, MATRIX11:1;
hence x in X by A36, A37, A40; :: thesis:

end;

A42: p29 .: (((finSeg i1) \ (f " Y)) \/ (((finSeg (N + 2)) \ (Seg i)) /\ (f " Y))) c= Seg j1

proof

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume y in p29 .: (((finSeg i1) \ (f " Y)) \/ (((finSeg (N + 2)) \ (Seg i)) /\ (f " Y))) ; :: thesis:
then consider x being object such that
A43: x in dom p29 and
A44: x in ((finSeg i1) \ (f " Y)) \/ (((finSeg (N + 2)) \ (Seg i)) /\ (f " Y)) and
A45: p29 . x = y by FUNCT_1:def 6;
dom p29 = Seg (N + 2) by FUNCT_2:52;
then consider k being Nat such that
A46: x = k and
A47: 1 <= k and
A48: k <= N + 2 by A43;

per cases by A44, A46, XBOOLE_0:def 3;

suppose A49: k in (finSeg i1) \ (f " Y) ; :: thesis:

then k <= i1 by FINSEQ_1:1;
then A50: k < i1 + 1 by NAT_1:13;
A51: finSeg i1 c= dom f by A8, XBOOLE_1:7;
A52: k in finSeg i1 by A49;
then A53: f . k in rng f by A51, FUNCT_1:def 3;
not k in f " Y by A49, XBOOLE_0:def 5;
then A54: not f . k in Y by A52, A51, FUNCT_1:def 7;
A55: k in Seg (N + 2) by A47, A48;
dom p29 = Seg (N + 2) by FUNCT_2:52;
then A56: p2 . i <> p2 . k by A1, A50, A55, FUNCT_1:def 4;
A57: f . k = H₁(k) by A8, A52, A51;
then H₁(k) in X by A34, A53;
then ex m being Nat st
( H₁(k) = {m,i} & {m,i} in 2Set (Seg (n + 2)) ) ;
then (Part_sgn (p2,K)) . {k,i} <> - (1_ K) by A34, A54, A53, A57;
then p2 . k <= p2 . i by A1, A50, A55, MATRIX11:def 1;
then p2 . k < j1 + 1 by A2, A56, XXREAL_0:1;
then A58: p2 . k <= j1 by NAT_1:13;
A59: rng p29 = Seg (N + 2) by FUNCT_2:def 3;
p2 . k in rng p29 by A43, A46, FUNCT_1:def 3;
then 1 <= p2 . k by A59, FINSEQ_1:1;
hence y in Seg j1 by A45, A46, A58; :: thesis:

end;

suppose A60: k in ((finSeg (N + 2)) \ (Seg i)) /\ (f " Y) ; :: thesis:

then k in (finSeg (N + 2)) \ (Seg i) by XBOOLE_0:def 4;
then A61: not k in Seg i by XBOOLE_0:def 5;
1 <= k by A60, FINSEQ_1:1;
then A62: i < k by A61;
A63: k in f " Y by A60, XBOOLE_0:def 4;
then f . k in Y by FUNCT_1:def 7;
then consider s being Element of 2Set (Seg (n + 2)) such that
A64: s = f . k and
s in X and
A65: (Part_sgn (p2,K)) . s = - (1_ K) ;
k in dom f by A63, FUNCT_1:def 7;
then A66: s = {i,k} by A8, A64;
dom p29 = finSeg (N + 2) by FUNCT_2:52;
then A67: p29 . i <> p2 . k by A1, A60, A62, FUNCT_1:def 4;
reconsider i = i, k = k as Element of NAT by ORDINAL1:def 12;
1_ K <> - (1_ K) by MATRIX11:22;
then p2 . i >= p2 . k by A1, A60, A65, A66, A62, MATRIX11:def 1;
then p2 . k < j1 + 1 by A2, A67, XXREAL_0:1;
then A68: p2 . k <= j1 by NAT_1:13;
A69: rng p29 = Seg (N + 2) by FUNCT_2:def 3;
p2 . k in rng p29 by A43, A46, FUNCT_1:def 3;
then 1 <= p2 . k by A69, FINSEQ_1:1;
hence y in Seg j1 by A45, A46, A68; :: thesis:

end;

take X ; :: thesis:
reconsider I = i, J = j as Element of NAT by ORDINAL1:def 12;
set P = power K;
thus X = { {e,i} where e is Nat : {e,i} in 2Set (Seg (n + 2)) } ; :: thesis:
A70: (finSeg i1) /\ (f " Y) c= finSeg i1 by XBOOLE_1:17;
Seg j1 c= p29 .: (((finSeg i1) \ (f " Y)) \/ (((finSeg (N + 2)) \ (Seg i)) /\ (f " Y)))

proof

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume A71: y in Seg j1 ; :: thesis:
consider k being Nat such that
A72: y = k and
1 <= k and
A73: k <= j1 by A71;
A74: j1 < j1 + 1 by NAT_1:13;
then A75: k < j by A73, XXREAL_0:2;
j <= N + 2 by A2, A7, A3, FINSEQ_1:1;
then j1 <= N + 2 by A74, XXREAL_0:2;
then Seg j1 c= Seg (N + 2) by FINSEQ_1:5;
then consider x being object such that
A76: x in dom p29 and
A77: y = p29 . x by A3, A71, FUNCT_1:def 3;
A78: not x in {i} by A2, A72, A73, A74, A77, TARSKI:def 1;
then A79: x in dom f by A33, A8, A76, XBOOLE_0:def 5;
then A80: f . x = H₁(x) by A8;
A81: f . x in rng f by A79, FUNCT_1:def 3;
then H₁(x) in X by A34, A80;
then consider m being Nat such that
A82: H₁(x) = {m,i} and
A83: {m,i} in 2Set (Seg (N + 2)) ;
A84: m <> i by A83, SGRAPH1:10;
A85: m in Seg (N + 2) by A83, SGRAPH1:10;
m in {x,i} by A82, TARSKI:def 2;
then A86: m = x by A84, TARSKI:def 2;
reconsider m = m, i = i as Element of NAT by ORDINAL1:def 12;

per cases by A83, SGRAPH1:10, XXREAL_0:1;

suppose A87: m < i ; :: thesis:

A88: not m in f " Y

proof

assume m in f " Y ; :: thesis:
then {m,i} in Y by A80, A86, FUNCT_1:def 7;
then A89: ex s being Element of 2Set (Seg (n + 2)) st
( s = {m,i} & s in X & (Part_sgn (p2,K)) . s = - (1_ K) ) ;
(Part_sgn (p2,K)) . {m,i} = 1_ K by A1, A2, A72, A75, A76, A77, A86, A87, MATRIX11:def 1;
hence contradiction by A89, MATRIX11:22; :: thesis:

end;

m < i1 + 1 by A87;
then A90: m <= i1 by NAT_1:13;
1 <= m by A85, FINSEQ_1:1;
then m in finSeg i1 by A90;
then x in (finSeg i1) \ (f " Y) by A86, A88, XBOOLE_0:def 5;
then x in ((finSeg i1) \ (f " Y)) \/ (((finSeg (N + 2)) \ (Seg i)) /\ (f " Y)) by XBOOLE_0:def 3;
hence y in p29 .: (((finSeg i1) \ (f " Y)) \/ (((finSeg (N + 2)) \ (Seg i)) /\ (f " Y))) by A76, A77, FUNCT_1:def 6; :: thesis:

end;

suppose A91: m > i ; :: thesis:

then not m in Seg i by FINSEQ_1:1;
then A92: x in (finSeg (N + 2)) \ (Seg i) by A86, A85, XBOOLE_0:def 5;
(Part_sgn (p2,K)) . {m,i} = - (1_ K) by A1, A2, A72, A75, A76, A77, A86, A91, MATRIX11:def 1;
then A93: f . x in Y by A34, A80, A81, A82, A83;
x in dom f by A33, A8, A76, A78, XBOOLE_0:def 5;
then x in f " Y by A93, FUNCT_1:def 7;
then x in ((finSeg (N + 2)) \ (Seg i)) /\ (f " Y) by A92, XBOOLE_0:def 4;
then x in ((finSeg i1) \ (f " Y)) \/ (((finSeg (N + 2)) \ (Seg i)) /\ (f " Y)) by XBOOLE_0:def 3;
hence y in p29 .: (((finSeg i1) \ (f " Y)) \/ (((finSeg (N + 2)) \ (Seg i)) /\ (f " Y))) by A76, A77, FUNCT_1:def 6; :: thesis:

end;

then A94: Seg j1 = p29 .: (((finSeg i1) \ (f " Y)) \/ (((finSeg (N + 2)) \ (Seg i)) /\ (f " Y))) by A42, XBOOLE_0:def 10;
A95: Seg (N + 2) = dom p29 by FUNCT_2:52;
A96: (finSeg i1) \ (f " Y) = (finSeg i1) \ ((f " Y) /\ (finSeg i1)) by XBOOLE_1:47;
i1 < i1 + 1 by NAT_1:13;
then finSeg i1 c= Seg i by FINSEQ_1:5;
then A97: finSeg i1 misses (finSeg (N + 2)) \ (Seg i) by XBOOLE_1:64, XBOOLE_1:79;
X c= rng f

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in X ; :: thesis:
then consider k being Nat such that
A98: x = {k,i} and
A99: {k,i} in 2Set (Seg (n + 2)) ;
k <> i by A99, SGRAPH1:10;
then A100: not k in {i} by TARSKI:def 1;
k in Seg (N + 2) by A99, SGRAPH1:10;
then A101: k in (finSeg i1) \/ ((finSeg (N + 2)) \ (Seg i)) by A33, A100, XBOOLE_0:def 5;
then f . k = H₁(k) by A8;
hence x in rng f by A8, A98, A101, FUNCT_1:def 3; :: thesis:

end;

then X = rng f by A34, XBOOLE_0:def 10;
then A102: f .: fY = Y by A5, FUNCT_1:77;
((finSeg i1) /\ (f " Y)) \/ (((finSeg (N + 2)) \ (Seg i)) /\ (f " Y)) = (dom f) /\ (f " Y) by A8, XBOOLE_1:23;
then A103: ((finSeg i1) /\ (f " Y)) \/ (((finSeg (N + 2)) \ (Seg i)) /\ (f " Y)) = f " Y by RELAT_1:132, XBOOLE_1:28;
A104: ((finSeg (N + 2)) \ (Seg i)) /\ (f " Y) c= (finSeg (N + 2)) \ (Seg i) by XBOOLE_1:17;
then ((finSeg i1) \ (f " Y)) \/ (((finSeg (N + 2)) \ (Seg i)) /\ (f " Y)) c= (finSeg (N + 2)) \ {i} by A33, XBOOLE_1:13;
then finSeg j1,((finSeg i1) \ (f " Y)) \/ (((finSeg (N + 2)) \ (Seg i)) /\ (f " Y)) are_equipotent by A95, A94, CARD_1:33, XBOOLE_1:1;
then A105: card (finSeg j1) = card (((finSeg i1) \ (f " Y)) \/ (((finSeg (N + 2)) \ (Seg i)) /\ (f " Y))) by CARD_1:5
.= (card ((finSeg i1) \ ((f " Y) /\ (finSeg i1)))) + (card (((finSeg (N + 2)) \ (Seg i)) /\ (f " Y))) by A97, A104, A96, CARD_2:40, XBOOLE_1:64
.= ((card (finSeg i1)) - (card ((f " Y) /\ (finSeg i1)))) + (card (((finSeg (N + 2)) \ (Seg i)) /\ (f " Y))) by CARD_2:44, XBOOLE_1:17 ;

per cases ;

suppose j > i ; :: thesis:

then reconsider ji = j - i as Element of NAT by NAT_1:21;
card Y = (((card ((finSeg i1) /\ fY)) + (card (finSeg j1))) - (card (finSeg i1))) + (card (fY /\ (finSeg i1))) by A97, A70, A104, A103, A26, A102, A105, CARD_2:40, XBOOLE_1:64
.= ((2 * (card ((finSeg i1) /\ fY))) + (card (finSeg j1))) - (card (finSeg i1))
.= ((2 * (card ((finSeg i1) /\ fY))) + j1) - (card (finSeg i1)) by FINSEQ_1:57
.= ((2 * (card ((finSeg i1) /\ fY))) + j1) - i1 by FINSEQ_1:57
.= (2 * (card ((finSeg i1) /\ fY))) + ji ;
hence the multF of K $$ (X,(Part_sgn (p2,K))) = (power K) . ((- (1_ K)),((2 * (card ((finSeg i1) /\ fY))) + ji)) by Th8
.= ((power K) . ((- (1_ K)),(2 * (card ((finSeg i1) /\ fY))))) * ((power K) . ((- (1_ K)),ji)) by HURWITZ:3
.= (1_ K) * ((power K) . ((- (1_ K)),ji)) by HURWITZ:4
.= ((power K) . ((- (1_ K)),(2 * I))) * ((power K) . ((- (1_ K)),ji)) by HURWITZ:4
.= (power K) . ((- (1_ K)),((2 * i) + ji)) by HURWITZ:3
.= (power K) . ((- (1_ K)),(i + j)) ;
:: thesis:

end;

suppose j <= i ; :: thesis:

then reconsider ij = i - j as Element of NAT by NAT_1:21;
card Y = (((card (finSeg i1)) + (card (((finSeg (N + 2)) \ (Seg i)) /\ fY))) - (card (finSeg j1))) + (card (((finSeg (N + 2)) \ (Seg i)) /\ fY)) by A97, A70, A104, A103, A26, A102, A105, CARD_2:40, XBOOLE_1:64
.= ((2 * (card (((finSeg (N + 2)) \ (Seg i)) /\ fY))) - (card (finSeg j1))) + (card (finSeg i1))
.= ((2 * (card (((finSeg (N + 2)) \ (Seg i)) /\ fY))) - j1) + (card (finSeg i1)) by FINSEQ_1:57
.= ((2 * (card (((finSeg (N + 2)) \ (Seg i)) /\ fY))) - j1) + i1 by FINSEQ_1:57
.= (2 * (card (((finSeg (N + 2)) \ (Seg i)) /\ fY))) + ij ;
hence the multF of K $$ (X,(Part_sgn (p2,K))) = (power K) . ((- (1_ K)),((2 * (card (((finSeg (N + 2)) \ (Seg i)) /\ fY))) + ij)) by Th8
.= ((power K) . ((- (1_ K)),(2 * (card (((finSeg (N + 2)) \ (Seg i)) /\ fY))))) * ((power K) . ((- (1_ K)),ij)) by HURWITZ:3
.= (1_ K) * ((power K) . ((- (1_ K)),ij)) by HURWITZ:4
.= ((power K) . ((- (1_ K)),(2 * J))) * ((power K) . ((- (1_ K)),ij)) by HURWITZ:4
.= (power K) . ((- (1_ K)),((2 * j) + ij)) by HURWITZ:3
.= (power K) . ((- (1_ K)),(i + j)) ;
:: thesis:

end;