theorem Th12: :: MATRIX11:12

for n being 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