for n being Nat
for K being Field
for i, j being Nat st i in Seg n & j in Seg n holds
for P being Element of Fin (Permutations n) st P = { p where p is Element of Permutations n : p . i = j } holds
for M being Matrix of n,K holds the addF of K $$ (P,(Path_product M)) = (M * (i,j)) * (Cofactor (M,i,j))