:: deftheorem defines Det MATRIX_3:def 9 :
for n being Nat
for K being Ring
for M being Matrix of n,K holds Det M = the addF of K $$ ((In ((Permutations n),(Fin (Permutations n)))),(Path_product M));