:: deftheorem Def1 defines PPath_product MATRIX_9:def 1 :
for n being Nat
for K being Field
for M being Matrix of n,K
for b₄ being Function of (Permutations n), the carrier of K holds
( b₄ = PPath_product M iff for p being Element of Permutations n holds b₄ . p = the multF of K $$ (Path_matrix (p,M)) );