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))) = () . ((- (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))) = () . ((- (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))) = () . ((- (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))) = () . ((- (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))) = () . ((- (1_ K)),(card Y))
reconsider ID = id (Seg (n + 2)) as Element of Permutations (n + 2) by MATRIX_1:def 12;
set Y9 = { s where s is Element of 2Set (Seg (n + 2)) : ( s in X & (Part_sgn (p2,K)) . s <> (Part_sgn (ID,K)) . s ) } ;
A2: for x being object st x in X holds
(Part_sgn (ID,K)) . x = 1_ K
proof
A3: X c= 2Set (Seg (n + 2)) by FINSUB_1:def 5;
let x be object ; :: thesis: ( x in X implies (Part_sgn (ID,K)) . x = 1_ K )
assume x in X ; :: thesis: (Part_sgn (ID,K)) . x = 1_ K
then consider i, j being Nat such that
A4: i in Seg (n + 2) and
A5: j in Seg (n + 2) and
A6: i < j and
A7: x = {i,j} by ;
A8: ID . j = j by ;
ID . i = i by ;
hence (Part_sgn (ID,K)) . x = 1_ K by ; :: thesis: verum
end;
A9: { 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 object ; :: 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
A10: y = s and
A11: s in X and
A12: (Part_sgn (p2,K)) . s <> (Part_sgn (ID,K)) . s ;
(Part_sgn (ID,K)) . s = 1_ K by ;
then (Part_sgn (p2,K)) . s = - (1_ K) by ;
hence y in Y by A1, A10, A11; :: thesis: verum
end;
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 object ; :: 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 ) } )
A13: 1_ K <> - (1_ K) by MATRIX11:22;
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
A14: s = y and
A15: s in X and
A16: (Part_sgn (p2,K)) . s = - (1_ K) by A1;
(Part_sgn (ID,K)) . s = 1_ K by ;
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 A14, A15, A16, A13; :: thesis: verum
end;
then A17: 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 ;
per cases ) mod 2 = 0 or (card Y) mod 2 = 1 ) by NAT_D:12;
suppose A18: (card Y) mod 2 = 0 ; :: thesis: the multF of K \$\$ (X,(Part_sgn (p2,K))) = () . ((- (1_ K)),(card Y))
then consider t being Nat such that
A19: card Y = (2 * t) + 0 and
0 < 2 by NAT_D:def 2;
t is Element of NAT by ORDINAL1:def 12;
hence () . ((- (1_ K)),(card Y)) = 1_ K by
.= the multF of K \$\$ (X,(Part_sgn (ID,K))) by
.= the multF of K \$\$ (X,(Part_sgn (p2,K))) by ;
:: thesis: verum
end;
suppose A20: (card Y) mod 2 = 1 ; :: thesis: the multF of K \$\$ (X,(Part_sgn (p2,K))) = () . ((- (1_ K)),(card Y))
then consider t being Nat such that
A21: card Y = (2 * t) + 1 and
1 < 2 by NAT_D:def 2;
t is Element of NAT by ORDINAL1:def 12;
hence () . ((- (1_ K)),(card Y)) = - (1_ K) by
.= - ( the multF of K \$\$ (X,(Part_sgn (ID,K)))) by
.= the multF of K \$\$ (X,(Part_sgn (p2,K))) by ;
:: thesis: verum
end;
end;