:: deftheorem defines Per MATRIX_9:def 2 :
for n being Nat
for K being Field
for M being Matrix of n,K holds Per M = the addF of K $$ ((In ((Permutations n),(Fin (Permutations n)))),(PPath_product M));