theorem Th9: :: MATRIX11:9

for n being Nat
for K being commutative Ring
for p2, q2, pq2 being Element of Permutations (n + 2)
for i, j being Nat st pq2 = p2 * q2 & q2 is being_transposition & q2 . i = j & i < j holds
for s being Element of 2Set (Seg (n + 2)) holds
( not (Part_sgn (p2,K)) . s <> (Part_sgn (pq2,K)) . s or i in s or j in s )