let n be Nat; :: thesis: for K being Fanoian Field

for p2 being Element of Permutations (n + 2)

for i, j being Nat st i in Seg (n + 2) & p2 . i = j holds

ex X being Element of Fin (2Set (Seg (n + 2))) st

( X = { {N,i} where N is Nat : {N,i} in 2Set (Seg (n + 2)) } & the multF of K $$ (X,(Part_sgn (p2,K))) = (power K) . ((- (1_ K)),(i + j)) )

let K be Fanoian Field; :: thesis: for p2 being Element of Permutations (n + 2)

for i, j being Nat st i in Seg (n + 2) & p2 . i = j holds

ex X being Element of Fin (2Set (Seg (n + 2))) st

( X = { {N,i} where N is Nat : {N,i} in 2Set (Seg (n + 2)) } & the multF of K $$ (X,(Part_sgn (p2,K))) = (power K) . ((- (1_ K)),(i + j)) )

let p2 be Element of Permutations (n + 2); :: thesis: for i, j being Nat st i in Seg (n + 2) & p2 . i = j holds

ex X being Element of Fin (2Set (Seg (n + 2))) st

( X = { {N,i} where N is Nat : {N,i} in 2Set (Seg (n + 2)) } & the multF of K $$ (X,(Part_sgn (p2,K))) = (power K) . ((- (1_ K)),(i + j)) )

let i, j be Nat; :: thesis: ( i in Seg (n + 2) & p2 . i = j implies ex X being Element of Fin (2Set (Seg (n + 2))) st

( X = { {N,i} where N is Nat : {N,i} in 2Set (Seg (n + 2)) } & the multF of K $$ (X,(Part_sgn (p2,K))) = (power K) . ((- (1_ K)),(i + j)) ) )

assume that

A1: i in Seg (n + 2) and

A2: p2 . i = j ; :: thesis: ex X being Element of Fin (2Set (Seg (n + 2))) st

( X = { {N,i} where N is Nat : {N,i} in 2Set (Seg (n + 2)) } & the multF of K $$ (X,(Part_sgn (p2,K))) = (power K) . ((- (1_ K)),(i + j)) )

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_{1}( 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))

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

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_{1}(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}

x1 = x2

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))

A34: rng f c= X

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: the multF of K $$ (X,(Part_sgn (p2,K))) = (power K) . ((- (1_ K)),(i + j))

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)))

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

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 ;

for p2 being Element of Permutations (n + 2)

for i, j being Nat st i in Seg (n + 2) & p2 . i = j holds

ex X being Element of Fin (2Set (Seg (n + 2))) st

( X = { {N,i} where N is Nat : {N,i} in 2Set (Seg (n + 2)) } & the multF of K $$ (X,(Part_sgn (p2,K))) = (power K) . ((- (1_ K)),(i + j)) )

let K be Fanoian Field; :: thesis: for p2 being Element of Permutations (n + 2)

for i, j being Nat st i in Seg (n + 2) & p2 . i = j holds

ex X being Element of Fin (2Set (Seg (n + 2))) st

( X = { {N,i} where N is Nat : {N,i} in 2Set (Seg (n + 2)) } & the multF of K $$ (X,(Part_sgn (p2,K))) = (power K) . ((- (1_ K)),(i + j)) )

let p2 be Element of Permutations (n + 2); :: thesis: for i, j being Nat st i in Seg (n + 2) & p2 . i = j holds

ex X being Element of Fin (2Set (Seg (n + 2))) st

( X = { {N,i} where N is Nat : {N,i} in 2Set (Seg (n + 2)) } & the multF of K $$ (X,(Part_sgn (p2,K))) = (power K) . ((- (1_ K)),(i + j)) )

let i, j be Nat; :: thesis: ( i in Seg (n + 2) & p2 . i = j implies ex X being Element of Fin (2Set (Seg (n + 2))) st

( X = { {N,i} where N is Nat : {N,i} in 2Set (Seg (n + 2)) } & the multF of K $$ (X,(Part_sgn (p2,K))) = (power K) . ((- (1_ K)),(i + j)) ) )

assume that

A1: i in Seg (n + 2) and

A2: p2 . i = j ; :: thesis: ex X being Element of Fin (2Set (Seg (n + 2))) st

( X = { {N,i} where N is Nat : {N,i} in 2Set (Seg (n + 2)) } & the multF of K $$ (X,(Part_sgn (p2,K))) = (power K) . ((- (1_ K)),(i + j)) )

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

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

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;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { {k,i} where k is Nat : {k,i} in 2Set (Seg (n + 2)) } or x in 2Set (Seg (n + 2)) )

assume x in { {k,i} where k is Nat : {k,i} in 2Set (Seg (n + 2)) } ; :: thesis: x in 2Set (Seg (n + 2))

then ex k being Nat st

( x = {k,i} & {k,i} in 2Set (Seg (N + 2)) ) ;

hence x in 2Set (Seg (n + 2)) ; :: thesis: verum

end;assume x in { {k,i} where k is Nat : {k,i} in 2Set (Seg (n + 2)) } ; :: thesis: x in 2Set (Seg (n + 2))

then ex k being Nat st

( x = {k,i} & {k,i} in 2Set (Seg (N + 2)) ) ;

hence x in 2Set (Seg (n + 2)) ; :: thesis: verum

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

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;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { s where s is Element of 2Set (Seg (n + 2)) : ( s in X & (Part_sgn (p2,K)) . s = - (1_ K) ) } or x in X )

assume x in { s where s is Element of 2Set (Seg (n + 2)) : ( s in X & (Part_sgn (p2,K)) . s = - (1_ K) ) } ; :: thesis: x in X

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

end;assume x in { s where s is Element of 2Set (Seg (n + 2)) : ( s in X & (Part_sgn (p2,K)) . s = - (1_ K) ) } ; :: thesis: x in X

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

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

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

for x1, x2 being object st x1 in dom f & x2 in dom f & f . x1 = f . x2 holds
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (finSeg i1) \/ ((finSeg (N + 2)) \ (Seg i)) or x in (Seg (N + 2)) \ {i} )

assume A11: x in (finSeg i1) \/ ((finSeg (N + 2)) \ (Seg i)) ; :: thesis: x in (Seg (N + 2)) \ {i}

end;assume A11: x in (finSeg i1) \/ ((finSeg (N + 2)) \ (Seg i)) ; :: thesis: x in (Seg (N + 2)) \ {i}

per cases
( x in finSeg i1 or x in (finSeg (N + 2)) \ (Seg i) )
by A11, XBOOLE_0:def 3;

end;

suppose A12:
x in finSeg i1
; :: thesis: x in (Seg (N + 2)) \ {i}

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

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

x1 = x2

proof

then
f is one-to-one
by FUNCT_1:def 4;
let x1, x2 be object ; :: thesis: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 implies x1 = x2 )

assume that

A21: x1 in dom f and

A22: x2 in dom f and

A23: f . x1 = f . x2 ; :: thesis: x1 = x2

A24: f . x2 = H_{1}(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_{1}(x1)
by A8, A21;

then x1 in {i,x2} by A23, A24, TARSKI:def 2;

hence x1 = x2 by A25, TARSKI:def 2; :: thesis: verum

end;assume that

A21: x1 in dom f and

A22: x2 in dom f and

A23: f . x1 = f . x2 ; :: thesis: x1 = x2

A24: f . x2 = H

not x1 in {i} by A10, A8, A21, XBOOLE_0:def 5;

then A25: x1 <> i by TARSKI:def 1;

f . x1 = H

then x1 in {i,x2} by A23, A24, TARSKI:def 2;

hence x1 = x2 by A25, TARSKI:def 2; :: thesis: verum

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

then A33:
(finSeg (N + 2)) \ {i} = (finSeg i1) \/ ((finSeg (N + 2)) \ (Seg i))
by A10, XBOOLE_0:def 10;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (finSeg (N + 2)) \ {i} or x in (finSeg i1) \/ ((finSeg (N + 2)) \ (Seg i)) )

assume A27: x in (finSeg (N + 2)) \ {i} ; :: thesis: x in (finSeg i1) \/ ((finSeg (N + 2)) \ (Seg i))

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;

end;assume A27: x in (finSeg (N + 2)) \ {i} ; :: thesis: x in (finSeg i1) \/ ((finSeg (N + 2)) \ (Seg i))

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
( k < i1 + 1 or k > i1 + 1 )
by A31, XXREAL_0:1;

end;

suppose
k < i1 + 1
; :: thesis: x in (finSeg i1) \/ ((finSeg (N + 2)) \ (Seg i))

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

end;then x in finSeg i1 by A28, A29;

hence x in (finSeg i1) \/ ((finSeg (N + 2)) \ (Seg i)) by XBOOLE_0:def 3; :: thesis: verum

suppose
k > i1 + 1
; :: thesis: x in (finSeg i1) \/ ((finSeg (N + 2)) \ (Seg i))

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

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

A34: rng f c= X

proof

A42:
p29 .: (((finSeg i1) \ (f " Y)) \/ (((finSeg (N + 2)) \ (Seg i)) /\ (f " Y))) c= Seg j1
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng f or x in X )

assume x in rng f ; :: thesis: x in X

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

end;assume x in rng f ; :: thesis: x in X

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

proof

take
X
; :: thesis: ( X = { {N,i} where N is Nat : {N,i} in 2Set (Seg (n + 2)) } & the multF of K $$ (X,(Part_sgn (p2,K))) = (power K) . ((- (1_ K)),(i + j)) )
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in p29 .: (((finSeg i1) \ (f " Y)) \/ (((finSeg (N + 2)) \ (Seg i)) /\ (f " Y))) or y in Seg j1 )

assume y in p29 .: (((finSeg i1) \ (f " Y)) \/ (((finSeg (N + 2)) \ (Seg i)) /\ (f " Y))) ; :: thesis: y in Seg j1

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;

end;assume y in p29 .: (((finSeg i1) \ (f " Y)) \/ (((finSeg (N + 2)) \ (Seg i)) /\ (f " Y))) ; :: thesis: y in Seg j1

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
( k in (finSeg i1) \ (f " Y) or k in ((finSeg (N + 2)) \ (Seg i)) /\ (f " Y) )
by A44, A46, XBOOLE_0:def 3;

end;

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

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_{1}(k)
by A8, A52, A51;

then H_{1}(k) in X
by A34, A53;

then ex m being Nat st

( H_{1}(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: verum

end;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

then H

then ex m being Nat st

( H

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

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

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

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

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: the multF of K $$ (X,(Part_sgn (p2,K))) = (power K) . ((- (1_ K)),(i + j))

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

then A94:
Seg j1 = p29 .: (((finSeg i1) \ (f " Y)) \/ (((finSeg (N + 2)) \ (Seg i)) /\ (f " Y)))
by A42, XBOOLE_0:def 10;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in Seg j1 or y in p29 .: (((finSeg i1) \ (f " Y)) \/ (((finSeg (N + 2)) \ (Seg i)) /\ (f " Y))) )

assume A71: y in Seg j1 ; :: thesis: y in p29 .: (((finSeg i1) \ (f " Y)) \/ (((finSeg (N + 2)) \ (Seg i)) /\ (f " Y)))

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_{1}(x)
by A8;

A81: f . x in rng f by A79, FUNCT_1:def 3;

then H_{1}(x) in X
by A34, A80;

then consider m being Nat such that

A82: H_{1}(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;

end;assume A71: y in Seg j1 ; :: thesis: y in p29 .: (((finSeg i1) \ (f " Y)) \/ (((finSeg (N + 2)) \ (Seg i)) /\ (f " Y)))

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

A81: f . x in rng f by A79, FUNCT_1:def 3;

then H

then consider m being Nat such that

A82: H

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
( m < i or m > i )
by A83, SGRAPH1:10, XXREAL_0:1;

end;

suppose A87:
m < i
; :: thesis: y in p29 .: (((finSeg i1) \ (f " Y)) \/ (((finSeg (N + 2)) \ (Seg i)) /\ (f " Y)))

A88:
not m in f " Y

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

end;proof

m < i1 + 1
by A87;
assume
m in f " Y
; :: thesis: contradiction

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

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

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

suppose A91:
m > i
; :: thesis: y in p29 .: (((finSeg i1) \ (f " Y)) \/ (((finSeg (N + 2)) \ (Seg i)) /\ (f " Y)))

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

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

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

then
X = rng f
by A34, XBOOLE_0:def 10;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in rng f )

assume x in X ; :: thesis: x in rng f

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_{1}(k)
by A8;

hence x in rng f by A8, A98, A101, FUNCT_1:def 3; :: thesis: verum

end;assume x in X ; :: thesis: x in rng f

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

hence x in rng f by A8, A98, A101, FUNCT_1:def 3; :: thesis: verum

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
( j > i or j <= i )
;

end;

suppose
j > i
; :: thesis: the multF of K $$ (X,(Part_sgn (p2,K))) = (power K) . ((- (1_ K)),(i + j))

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

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

suppose
j <= i
; :: thesis: the multF of K $$ (X,(Part_sgn (p2,K))) = (power K) . ((- (1_ K)),(i + j))

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

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