let n be Nat; :: thesis: for K being commutative Ring
for p2 being Element of Permutations (n + 2) holds
( sgn (p2,K) = 1_ K or sgn (p2,K) = - (1_ K) )
let K be commutative Ring; :: thesis: for p2 being Element of Permutations (n + 2) holds
( sgn (p2,K) = 1_ K or sgn (p2,K) = - (1_ K) )
let p2 be Element of Permutations (n + 2); :: thesis: ( sgn (p2,K) = 1_ K or sgn (p2,K) = - (1_ K) )
set KK = the carrier of K;
set n2 = n + 2;
set 2S = 2Set (Seg (n + 2));
set mm = the multF of K;
set Path = Part_sgn (p2,K);
2Set (Seg (n + 2)) in Fin (2Set (Seg (n + 2))) by FINSUB_1:def 5;
then In ((2Set (Seg (n + 2))),(Fin (2Set (Seg (n + 2))))) = 2Set (Seg (n + 2)) by SUBSET_1:def 8;
then reconsider 2S9 = 2Set (Seg (n + 2)) as Element of Fin (2Set (Seg (n + 2))) ;
consider G being Function of (Fin (2Set (Seg (n + 2)))), the carrier of K such that
A2: the multF of K $$ (2S9,(Part_sgn (p2,K))) = G . 2S9 and
A3: for e being Element of the carrier of K st e is_a_unity_wrt the multF of K holds
G . {} = e and
A4: for s being Element of 2Set (Seg (n + 2)) holds G . {s} = (Part_sgn (p2,K)) . s and
A5: for B being Element of Fin (2Set (Seg (n + 2))) st B c= 2S9 & B <> {} holds
for s being Element of 2Set (Seg (n + 2)) st s in 2S9 \ B holds
G . (B \/ {s}) = the multF of K . ((G . B),((Part_sgn (p2,K)) . s)) by SETWISEO:def 3;
defpred S₁[ Nat] means for B being Element of Fin (2Set (Seg (n + 2))) st card B = $1 & B c= 2Set (Seg (n + 2)) & not G . B = 1_ K holds
G . B = - (1_ K);
A6: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A7: S₁[k] ; :: thesis: S₁[k + 1]
set k1 = k + 1;
let B be Element of Fin (2Set (Seg (n + 2))); :: thesis: ( card B = k + 1 & B c= 2Set (Seg (n + 2)) & not G . B = 1_ K implies G . B = - (1_ K) )
assume that
A8: card B = k + 1 and
A9: B c= 2Set (Seg (n + 2)) ; :: thesis: ( G . B = 1_ K or G . B = - (1_ K) )

now :: thesis: ( ( k = 0 & ( G . B = 1_ K or G . B = - (1_ K) ) ) or ( k > 0 & ( G . B = 1_ K or G . B = - (1_ K) ) ) )

per cases ( k = 0 or k > 0 ) ;

case k = 0 ; :: thesis: ( G . B = 1_ K or G . B = - (1_ K) )

then consider x being object such that
A10: B = {x} by A8, CARD_2:42;
x in B by A10, TARSKI:def 1;
then reconsider x = x as Element of 2Set (Seg (n + 2)) by A9;
G . B = (Part_sgn (p2,K)) . x by A4, A10;
hence ( G . B = 1_ K or G . B = - (1_ K) ) by Th5; :: thesis: verum

end;

case A11: k > 0 ; :: thesis: ( G . B = 1_ K or G . B = - (1_ K) )

consider x being object such that
A12: x in B by A8, CARD_1:27, XBOOLE_0:def 1;
reconsider x = x as Element of 2Set (Seg (n + 2)) by A9, A12;
B \ {x} c= 2Set (Seg (n + 2)) by A9;
then reconsider B9 = B \ {x} as Element of Fin (2Set (Seg (n + 2))) by FINSUB_1:def 5;
A13: not x in B9 by ZFMISC_1:56;
A14: {x} \/ B9 = B by A12, ZFMISC_1:116;
then A15: k + 1 = (card B9) + 1 by A8, A13, CARD_2:41;
then A16: ( G . B9 = 1_ K or G . B9 = - (1_ K) ) by A7, A9, XBOOLE_1:1;
x in (2Set (Seg (n + 2))) \ B9 by A13, XBOOLE_0:def 5;
then G . B = the multF of K . ((G . B9),((Part_sgn (p2,K)) . x)) by A5, A9, A11, A14, A15, CARD_1:27, XBOOLE_1:1;
then ( G . B = (1_ K) * (1_ K) or G . B = (1_ K) * (- (1_ K)) or G . B = (- (1_ K)) * (1_ K) or G . B = (- (1_ K)) * (- (1_ K)) ) by A16, Th5;
then ( G . B = (1_ K) * (1_ K) or G . B = (1_ K) * (- (1_ K)) ) by VECTSP_1:10;
hence ( G . B = 1_ K or G . B = - (1_ K) ) ; :: thesis: verum

end;

end;

end;

hence ( G . B = 1_ K or G . B = - (1_ K) ) ; :: thesis: verum

end;

A17: S₁[ 0 ]

proof

let B be Element of Fin (2Set (Seg (n + 2))); :: thesis: ( card B = 0 & B c= 2Set (Seg (n + 2)) & not G . B = 1_ K implies G . B = - (1_ K) )
assume that
A18: card B = 0 and
B c= 2Set (Seg (n + 2)) ; :: thesis: ( G . B = 1_ K or G . B = - (1_ K) )
B = {} by A18;
hence ( G . B = 1_ K or G . B = - (1_ K) ) by A3, FVSUM_1:4; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A17, A6);
then S₁[ card 2S9] ;
hence ( sgn (p2,K) = 1_ K or sgn (p2,K) = - (1_ K) ) by A2; :: thesis: verum