let n be Nat; :: thesis: for K being Fanoian Field
for p2 being Element of Permutations (n + 2)
for X, Y being Element of Fin (2Set (Seg (n + 2))) st Y = { s where s is Element of 2Set (Seg (n + 2)) : ( s in X & (Part_sgn p2,K) . s = - (1_ K) ) } holds
the multF of K $$ X,(Part_sgn p2,K) = (power K) . (- (1_ K)),(card Y)
let K be Fanoian Field; :: thesis: for p2 being Element of Permutations (n + 2)
for X, Y being Element of Fin (2Set (Seg (n + 2))) st Y = { s where s is Element of 2Set (Seg (n + 2)) : ( s in X & (Part_sgn p2,K) . s = - (1_ K) ) } holds
the multF of K $$ X,(Part_sgn p2,K) = (power K) . (- (1_ K)),(card Y)
let p2 be Element of Permutations (n + 2); :: thesis: for X, Y being Element of Fin (2Set (Seg (n + 2))) st Y = { s where s is Element of 2Set (Seg (n + 2)) : ( s in X & (Part_sgn p2,K) . s = - (1_ K) ) } holds
the multF of K $$ X,(Part_sgn p2,K) = (power K) . (- (1_ K)),(card Y)
set n2 = n + 2;
let X, Y be Element of Fin (2Set (Seg (n + 2))); :: thesis: ( Y = { s where s is Element of 2Set (Seg (n + 2)) : ( s in X & (Part_sgn p2,K) . s = - (1_ K) ) } implies the multF of K $$ X,(Part_sgn p2,K) = (power K) . (- (1_ K)),(card Y) )
assume A1: Y = { s where s is Element of 2Set (Seg (n + 2)) : ( s in X & (Part_sgn p2,K) . s = - (1_ K) ) } ; :: thesis: the multF of K $$ X,(Part_sgn p2,K) = (power K) . (- (1_ K)),(card Y)
reconsider ID = id (Seg (n + 2)) as Element of Permutations (n + 2) by MATRIX_2:def 11;
A2: for x being set st x in X holds
(Part_sgn ID,K) . x = 1_ K

proof

let x be set ; :: thesis: ( x in X implies (Part_sgn ID,K) . x = 1_ K )
assume A3: x in X ; :: thesis: (Part_sgn ID,K) . x = 1_ K
X c= 2Set (Seg (n + 2)) by FINSUB_1:def 5;
then consider i, j being Nat such that
A4: ( i in Seg (n + 2) & j in Seg (n + 2) & i < j & x = {i,j} ) by A3, MATRIX11:1;
( ID . i = i & ID . j = j ) by A4, FUNCT_1:34;
hence (Part_sgn ID,K) . x = 1_ K by A4, MATRIX11:def 1; :: thesis: verum

end;

set Y' = { s where s is Element of 2Set (Seg (n + 2)) : ( s in X & (Part_sgn p2,K) . s <> (Part_sgn ID,K) . s ) } ;
A5: Y c= { s where s is Element of 2Set (Seg (n + 2)) : ( s in X & (Part_sgn p2,K) . s <> (Part_sgn ID,K) . s ) }

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in Y or y in { s where s is Element of 2Set (Seg (n + 2)) : ( s in X & (Part_sgn p2,K) . s <> (Part_sgn ID,K) . s ) } )
assume y in Y ; :: thesis: y in { s where s is Element of 2Set (Seg (n + 2)) : ( s in X & (Part_sgn p2,K) . s <> (Part_sgn ID,K) . s ) }
then consider s being Element of 2Set (Seg (n + 2)) such that
A6: ( s = y & s in X & (Part_sgn p2,K) . s = - (1_ K) ) by A1;
( (Part_sgn ID,K) . s = 1_ K & 1_ K <> - (1_ K) ) by A2, A6, MATRIX11:22;
hence y in { s where s is Element of 2Set (Seg (n + 2)) : ( s in X & (Part_sgn p2,K) . s <> (Part_sgn ID,K) . s ) } by A6; :: thesis: verum

end;

{ s where s is Element of 2Set (Seg (n + 2)) : ( s in X & (Part_sgn p2,K) . s <> (Part_sgn ID,K) . s ) } c= Y

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in { s where s is Element of 2Set (Seg (n + 2)) : ( s in X & (Part_sgn p2,K) . s <> (Part_sgn ID,K) . s ) } or y in Y )
assume y in { s where s is Element of 2Set (Seg (n + 2)) : ( s in X & (Part_sgn p2,K) . s <> (Part_sgn ID,K) . s ) } ; :: thesis: y in Y
then consider s being Element of 2Set (Seg (n + 2)) such that
A7: ( y = s & s in X & (Part_sgn p2,K) . s <> (Part_sgn ID,K) . s ) ;
(Part_sgn ID,K) . s = 1_ K by A2, A7;
then (Part_sgn p2,K) . s = - (1_ K) by A7, MATRIX11:5;
hence y in Y by A1, A7; :: thesis: verum

end;

then A8: Y = { s where s is Element of 2Set (Seg (n + 2)) : ( s in X & (Part_sgn p2,K) . s <> (Part_sgn ID,K) . s ) } by A5, XBOOLE_0:def 10;

per cases ( (card Y) mod 2 = 0 or (card Y) mod 2 = 1 ) by NAT_D:12;

suppose A9: (card Y) mod 2 = 0 ; :: thesis: the multF of K $$ X,(Part_sgn p2,K) = (power K) . (- (1_ K)),(card Y)

then consider t being Nat such that
A10: ( card Y = (2 * t) + 0 & 0 < 2 ) by NAT_D:def 2;
t is Element of NAT by ORDINAL1:def 13;
hence (power K) . (- (1_ K)),(card Y) = 1_ K by A10, HURWITZ:4
.= the multF of K $$ X,(Part_sgn ID,K) by A2, MATRIX11:4
.= the multF of K $$ X,(Part_sgn p2,K) by A8, A9, MATRIX11:7 ;
:: thesis: verum

end;

suppose A11: (card Y) mod 2 = 1 ; :: thesis: the multF of K $$ X,(Part_sgn p2,K) = (power K) . (- (1_ K)),(card Y)

then consider t being Nat such that
A12: ( card Y = (2 * t) + 1 & 1 < 2 ) by NAT_D:def 2;
t is Element of NAT by ORDINAL1:def 13;
hence (power K) . (- (1_ K)),(card Y) = - (1_ K) by A12, HURWITZ:4
.= - (the multF of K $$ X,(Part_sgn ID,K)) by A2, MATRIX11:4
.= the multF of K $$ X,(Part_sgn p2,K) by A8, A11, MATRIX11:7 ;
:: thesis: verum

end;

end;