let n be Nat; 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; 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); ( Id = idseq (n + 2) implies sgn (Id,K) = 1_ K )
assume A1:
Id = idseq (n + 2)
; 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 for x being object st x in 2S9 holds
(Part_sgn (Id,K)) . x = 1_ Klet x be
object ;
( x in 2S9 implies (Part_sgn (Id,K)) . x = 1_ K )assume
x in 2S9
;
(Part_sgn (Id,K)) . x = 1_ Kthen 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;
verum end;
hence
sgn (Id,K) = 1_ K
by Th4; verum