let n be Nat; :: thesis:
let K be commutative Ring; :: thesis:
let p2 be Element of Permutations (n + 2); :: thesis:
let X be Element of Fin (2Set (Seg (n + 2))); :: thesis:
assume A1: for x being object st x in X holds
(Part_sgn (p2,K)) . x = 1_ K ; :: thesis:
set Path = Part_sgn (p2,K);
set 2S = 2Set (Seg (n + 2));
set KK = the carrier of K;
set mm = the multF of K;
consider G being Function of (Fin (2Set (Seg (n + 2)))), the carrier of K such that
A2: the multF of K $$ (X,(Part_sgn (p2,K))) = G . X 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 x being Element of 2Set (Seg (n + 2)) holds G . {x} = (Part_sgn (p2,K)) . x and
A5: for B being Element of Fin (2Set (Seg (n + 2))) st B c= X & B <> {} holds
for x being Element of 2Set (Seg (n + 2)) st x in X \ B holds
G . (B \/ {x}) = the multF of K . ((G . B),((Part_sgn (p2,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= X holds
G . B = 1_ K;
A6: for k being Nat st S₁[k] holds
S₁[k + 1]

let k be Nat; :: thesis:
assume A7: S₁[k] ; :: thesis:
set k1 = k + 1;
let B be Element of Fin (2Set (Seg (n + 2))); :: thesis:
assume that
A8: card B = k + 1 and
A9: B c= X ; :: thesis:

then consider x being object such that
A10: B = {x} by A8, CARD_2:42;
A11: x in B by A10, 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 A11;
G . B = (Part_sgn (p2,K)) . x by A4, A10;
hence G . B = 1_ K by A1, A9, A11; :: thesis:

end;

end;

hence G . B = 1_ K ; :: thesis:

end;

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

end;