let n be Nat; :: thesis:
let K be commutative Ring; :: thesis:
let X be Element of Fin (2Set (Seg (n + 2))); :: thesis:
let p2, q2 be Element of Permutations (n + 2); :: thesis:
let F be finite set ; :: thesis:
assume A1: F = { s where s is Element of 2Set (Seg (n + 2)) : ( s in X & (Part_sgn (p2,K)) . s <> (Part_sgn (q2,K)) . s ) } ; :: thesis:
set Pq = Part_sgn (q2,K);
set Pp = Part_sgn (p2,K);
set 2S = 2Set (Seg (n + 2));
X c= 2Set (Seg (n + 2)) by FINSUB_1:def 5;
then X \ F c= 2Set (Seg (n + 2)) ;
then reconsider Y = X \ F as Element of Fin (2Set (Seg (n + 2))) by FINSUB_1:def 5;
A2: F c= X

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in F ; :: thesis:
then ex s being Element of 2Set (Seg (n + 2)) st
( x = s & s in X & (Part_sgn (p2,K)) . s <> (Part_sgn (q2,K)) . s ) by A1;
hence x in X ; :: thesis:

end;

then A3: F \/ Y = X by XBOOLE_1:45;
X c= 2Set (Seg (n + 2)) by FINSUB_1:def 5;
then F c= 2Set (Seg (n + 2)) by A2;
then reconsider F9 = F as Element of Fin (2Set (Seg (n + 2))) by FINSUB_1:def 5;
set KK = the carrier of K;
set mm = the multF of K;
consider Gp being Function of (Fin (2Set (Seg (n + 2)))), the carrier of K such that
A4: the multF of K $$ (F9,(Part_sgn (p2,K))) = Gp . F and
A5: for e being Element of the carrier of K st e is_a_unity_wrt the multF of K holds
Gp . {} = e and
A6: for x being Element of 2Set (Seg (n + 2)) holds Gp . {x} = (Part_sgn (p2,K)) . x and
A7: for B being Element of Fin (2Set (Seg (n + 2))) st B c= F & B <> {} holds
for x being Element of 2Set (Seg (n + 2)) st x in F9 \ B holds
Gp . (B \/ {x}) = the multF of K . ((Gp . B),((Part_sgn (p2,K)) . x)) by SETWISEO:def 3;
A8: Y c= 2Set (Seg (n + 2)) by FINSUB_1:def 5;
consider Gq being Function of (Fin (2Set (Seg (n + 2)))), the carrier of K such that
A9: the multF of K $$ (F9,(Part_sgn (q2,K))) = Gq . F and
A10: for e being Element of the carrier of K st e is_a_unity_wrt the multF of K holds
Gq . {} = e and
A11: for x being Element of 2Set (Seg (n + 2)) holds Gq . {x} = (Part_sgn (q2,K)) . x and
A12: for B being Element of Fin (2Set (Seg (n + 2))) st B c= F & B <> {} holds
for x being Element of 2Set (Seg (n + 2)) st x in F \ B holds
Gq . (B \/ {x}) = the multF of K . ((Gq . B),((Part_sgn (q2,K)) . x)) by SETWISEO:def 3;
defpred S₁[ Nat] means for B being Element of Fin (2Set (Seg (n + 2))) st card B = $1 & B c= F holds
( ( (card B) mod 2 = 0 implies Gp . B = Gq . B ) & ( (card B) mod 2 = 1 implies Gp . B = - (Gq . B) ) );
A13: for s being Element of 2Set (Seg (n + 2)) st s in F holds
(Part_sgn (p2,K)) . s = - ((Part_sgn (q2,K)) . s)

proof

let s be Element of 2Set (Seg (n + 2)); :: thesis:
assume s in F ; :: thesis:
then A14: ex s9 being Element of 2Set (Seg (n + 2)) st
( s9 = s & s9 in X & (Part_sgn (p2,K)) . s9 <> (Part_sgn (q2,K)) . s9 ) by A1;
A15: ( (Part_sgn (q2,K)) . s = 1_ K or (Part_sgn (q2,K)) . s = - (1_ K) ) by Th5;
( (Part_sgn (p2,K)) . s = 1_ K or (Part_sgn (p2,K)) . s = - (1_ K) ) by Th5;
then ((Part_sgn (p2,K)) . s) + ((Part_sgn (q2,K)) . s) = 0. K by A14, A15, RLVECT_1:def 10;
hence (Part_sgn (p2,K)) . s = - ((Part_sgn (q2,K)) . s) by VECTSP_1:16; :: thesis:

end;

A16: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis:
assume A17: S₁[k] ; :: thesis:
set k1 = k + 1;
let B be Element of Fin (2Set (Seg (n + 2))); :: thesis:
assume that
A18: card B = k + 1 and
A19: B c= F ; :: thesis:

now :: thesis:

per cases ;

case A20: k = 0 ; :: thesis:

then consider x being object such that
A21: B = {x} by A18, CARD_2:42;
A22: x in B by A21, TARSKI:def 1;
B c= 2Set (Seg (n + 2)) by FINSUB_1:def 5;
then reconsider x = x as Element of 2Set (Seg (n + 2)) by A22;
A23: Gq . B = (Part_sgn (q2,K)) . x by A11, A21;
Gp . B = (Part_sgn (p2,K)) . x by A6, A21;
hence ( ( (card B) mod 2 = 0 implies Gp . B = Gq . B ) & ( (card B) mod 2 = 1 implies Gp . B = - (Gq . B) ) ) by A13, A18, A19, A20, A22, A23, NAT_D:14; :: thesis:

end;

case A24: k > 0 ; :: thesis:

consider x being object such that
A25: x in B by A18, CARD_1:27, XBOOLE_0:def 1;
B c= 2Set (Seg (n + 2)) by FINSUB_1:def 5;
then reconsider x = x as Element of 2Set (Seg (n + 2)) by A25;
B c= 2Set (Seg (n + 2)) by FINSUB_1:def 5;
then B \ {x} c= 2Set (Seg (n + 2)) ;
then reconsider B9 = B \ {x} as Element of Fin (2Set (Seg (n + 2))) by FINSUB_1:def 5;
A26: not x in B9 by ZFMISC_1:56;
then A27: x in F \ B9 by A19, A25, XBOOLE_0:def 5;
A28: B9 c= F by A19;
A29: {x} \/ B9 = B by A25, ZFMISC_1:116;
then A30: k + 1 = (card B9) + 1 by A18, A26, CARD_2:41;
then A31: Gq . B = the multF of K . ((Gq . B9),((Part_sgn (q2,K)) . x)) by A12, A19, A24, A29, A27, CARD_1:27, XBOOLE_1:1;
A32: Gp . B = the multF of K . ((Gp . B9),((Part_sgn (p2,K)) . x)) by A7, A19, A24, A29, A30, A27, CARD_1:27, XBOOLE_1:1;

now :: thesis:

per cases by NAT_D:12;

case A33: k mod 2 = 0 ; :: thesis:

0 < 2 - 1 ;
then A34: (k + 1) mod 2 = 0 + 1 by A33, NAT_D:70;
A35: Gp . B = (Gp . B9) * (- ((Part_sgn (q2,K)) . x)) by A13, A19, A25, A32;
Gq . B = (Gp . B9) * ((Part_sgn (q2,K)) . x) by A17, A30, A28, A31, A33;
hence ( ( (card B) mod 2 = 0 implies Gp . B = Gq . B ) & ( (card B) mod 2 = 1 implies Gp . B = - (Gq . B) ) ) by A18, A35, A34, VECTSP_1:8; :: thesis:

end;

case A36: k mod 2 = 1 ; :: thesis:

A37: (Part_sgn (p2,K)) . x = - ((Part_sgn (q2,K)) . x) by A13, A19, A25;
Gp . B9 = - (Gq . B9) by A17, A30, A28, A36;
then A38: Gp . B = (- (Gq . B9)) * (- ((Part_sgn (q2,K)) . x)) by A7, A19, A24, A29, A30, A27, A37, CARD_1:27, XBOOLE_1:1;
A39: 2 - 1 = 1 ;
Gq . B = (Gq . B9) * ((Part_sgn (q2,K)) . x) by A12, A19, A24, A29, A30, A27, CARD_1:27, XBOOLE_1:1;
hence ( ( (card B) mod 2 = 0 implies Gp . B = Gq . B ) & ( (card B) mod 2 = 1 implies Gp . B = - (Gq . B) ) ) by A18, A36, A38, A39, NAT_D:69, VECTSP_1:10; :: thesis:

end;

hence ( ( (card B) mod 2 = 0 implies Gp . B = Gq . B ) & ( (card B) mod 2 = 1 implies Gp . B = - (Gq . B) ) ) ; :: thesis:

end;

hence ( ( (card B) mod 2 = 0 implies Gp . B = Gq . B ) & ( (card B) mod 2 = 1 implies Gp . B = - (Gq . B) ) ) ; :: thesis:

end;

A40: S₁[ 0 ]

proof

let B be Element of Fin (2Set (Seg (n + 2))); :: thesis:
assume that
A41: card B = 0 and
B c= F ; :: thesis:
A42: 0 = 0 mod 2 by NAT_D:26;
A43: B = {} by A41;
then Gp . B = 1_ K by A5, FVSUM_1:4;
hence ( ( (card B) mod 2 = 0 implies Gp . B = Gq . B ) & ( (card B) mod 2 = 1 implies Gp . B = - (Gq . B) ) ) by A10, A43, A42, FVSUM_1:4; :: thesis:

end;

A44: for k being Nat holds S₁[k] from NAT_1:sch 2(A40, A16);
A45: Y misses F by XBOOLE_1:79;
then A46: the multF of K $$ (X,(Part_sgn (p2,K))) = the multF of K . (( the multF of K $$ (Y,(Part_sgn (p2,K)))),( the multF of K $$ (F9,(Part_sgn (p2,K))))) by A3, SETWOP_2:4;
A47: the multF of K $$ (X,(Part_sgn (q2,K))) = the multF of K . (( the multF of K $$ (Y,(Part_sgn (q2,K)))),( the multF of K $$ (F9,(Part_sgn (q2,K))))) by A45, A3, SETWOP_2:4;
A48: dom (Part_sgn (p2,K)) = 2Set (Seg (n + 2)) by FUNCT_2:def 1;
then A49: dom ((Part_sgn (p2,K)) | Y) = Y by A8, RELAT_1:62;
dom (Part_sgn (q2,K)) = 2Set (Seg (n + 2)) by FUNCT_2:def 1;
then A50: dom ((Part_sgn (q2,K)) | Y) = Y by A8, RELAT_1:62;
for x being object st x in dom ((Part_sgn (p2,K)) | Y) holds
((Part_sgn (p2,K)) | Y) . x = ((Part_sgn (q2,K)) | Y) . x

proof

let x be object ; :: thesis:
assume A51: x in dom ((Part_sgn (p2,K)) | Y) ; :: thesis:
Y c= 2Set (Seg (n + 2)) by FINSUB_1:def 5;
then reconsider x9 = x as Element of 2Set (Seg (n + 2)) by A49, A51;
A52: ((Part_sgn (p2,K)) | Y) . x9 = (Part_sgn (p2,K)) . x9 by A51, FUNCT_1:47;
A53: not x9 in F by A49, A51, XBOOLE_0:def 5;
assume A54: ((Part_sgn (p2,K)) | Y) . x <> ((Part_sgn (q2,K)) | Y) . x ; :: thesis:
((Part_sgn (q2,K)) | Y) . x9 = (Part_sgn (q2,K)) . x9 by A49, A50, A51, FUNCT_1:47;
hence contradiction by A1, A49, A51, A54, A52, A53; :: thesis:

end;

then A55: (Part_sgn (p2,K)) | Y = (Part_sgn (q2,K)) | Y by A48, A8, A50, FUNCT_1:2, RELAT_1:62;
then A56: the multF of K $$ (Y,(Part_sgn (p2,K))) = the multF of K $$ (Y,(Part_sgn (q2,K))) by SETWOP_2:7;

now :: thesis:

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

case (card F) mod 2 = 0 ; :: thesis:

hence ( ( (card F) mod 2 = 0 implies the multF of K $$ (X,(Part_sgn (p2,K))) = the multF of K $$ (X,(Part_sgn (q2,K))) ) & ( (card F) mod 2 = 1 implies the multF of K $$ (X,(Part_sgn (p2,K))) = - ( the multF of K $$ (X,(Part_sgn (q2,K)))) ) ) by A4, A9, A44, A56, A46, A47; :: thesis:

end;

case A57: (card F) mod 2 = 1 ; :: thesis:

A58: the multF of K $$ (X,(Part_sgn (q2,K))) = ( the multF of K $$ (Y,(Part_sgn (p2,K)))) * ( the multF of K $$ (F9,(Part_sgn (q2,K)))) by A55, A47, SETWOP_2:7;
the multF of K $$ (X,(Part_sgn (p2,K))) = ( the multF of K $$ (Y,(Part_sgn (p2,K)))) * (- ( the multF of K $$ (F9,(Part_sgn (q2,K))))) by A4, A9, A44, A46, A57;
hence ( ( (card F) mod 2 = 0 implies the multF of K $$ (X,(Part_sgn (p2,K))) = the multF of K $$ (X,(Part_sgn (q2,K))) ) & ( (card F) mod 2 = 1 implies the multF of K $$ (X,(Part_sgn (p2,K))) = - ( the multF of K $$ (X,(Part_sgn (q2,K)))) ) ) by A57, A58, VECTSP_1:8; :: thesis:

end;