for n being Nat
for K being commutative Ring
for p2, q2 being Element of Permutations (n + 2)
for i, j being Nat st i in Seg (n + 2) & j in Seg (n + 2) & i < j & p2 . i = q2 . i & p2 . j = q2 . j holds
(Part_sgn (p2,K)) . {i,j} = (Part_sgn (q2,K)) . {i,j}