for n being Nat
for K being commutative Ring
for p2 being Element of Permutations (n + 2)
for s being Element of 2Set (Seg (n + 2)) holds
( (Part_sgn (p2,K)) . s = 1_ K or (Part_sgn (p2,K)) . s = - (1_ K) )