let n be Nat; :: thesis: for K being commutative Ring
for Id being Element of Permutations (n + 2) st Id = idseq (n + 2) holds
sgn (Id,K) = 1_ K
let K be commutative Ring; :: 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));
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))) ;

now :: thesis: for x being object st x in 2S9 holds
(Part_sgn (Id,K)) . x = 1_ K

let x be object ; :: 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:18;
Id . i = i by A1, A3, FUNCT_1:18;
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 Th4; :: thesis: verum