:: deftheorem Def8 defines Path_product MATRIX_3:def 8 :
for n being Nat
for K being Ring
for M being Matrix of n,K
for b₄ being Function of (Permutations n), the carrier of K holds
( b₄ = Path_product M iff for p being Element of Permutations n holds b₄ . p = - (( the multF of K $$ (Path_matrix (p,M))),p) );