:: deftheorem defines sgn MATRIX11:def 2 :
for n being Nat
for K being commutative Ring
for perm2 being Element of Permutations (n + 2) holds sgn (perm2,K) = the multF of K $$ ((In ((2Set (Seg (n + 2))),(Fin (2Set (Seg (n + 2)))))),(Part_sgn (perm2,K)));