let n be Nat; :: thesis: for K being Field
for Id being Element of Permutations (n + 2) st Id = idseq (n + 2) holds
sgn Id,K = 1_ K
let K be Field; :: thesis: for Id being Element of Permutations (n + 2) st Id = idseq (n + 2) holds
sgn Id,K = 1_ K
set n2 = n + 2;
let Id be Element of Permutations (n + 2); :: thesis: ( Id = idseq (n + 2) implies sgn Id,K = 1_ K )
assume A1: Id = idseq (n + 2) ; :: thesis: sgn Id,K = 1_ K
set Path = Part_sgn Id,K;
set 2S = 2Set (Seg (n + 2));
A2: FinOmega (2Set (Seg (n + 2))) = 2Set (Seg (n + 2)) by MATRIX_2:def 17;
then reconsider 2S9 = 2Set (Seg (n + 2)) as Element of Fin (2Set (Seg (n + 2))) ;

now

let x be set ; :: thesis: ( x in 2S9 implies (Part_sgn Id,K) . x = 1_ K )
assume x in 2S9 ; :: thesis: (Part_sgn Id,K) . x = 1_ K
then consider i, j being Nat such that
A3: i in Seg (n + 2) and
A4: j in Seg (n + 2) and
A5: i < j and
A6: x = {i,j} by Th1;
A7: Id . j = j by A1, A4, FUNCT_1:35;
Id . i = i by A1, A3, FUNCT_1:35;
hence (Part_sgn Id,K) . x = 1_ K by A3, A4, A5, A6, A7, Def1; :: thesis: verum

end;

hence sgn Id,K = 1_ K by A2, Th4; :: thesis: verum