:: deftheorem Def7 defines Path_matrix MATRIX_3:def 7 :
for n being Nat
for K being Ring
for M being Matrix of n,K
for p being Element of Permutations n
for b₅ being FinSequence of K holds
( b₅ = Path_matrix (p,M) iff ( len b₅ = n & ( for i, j being Nat st i in dom b₅ & j = p . i holds
b₅ . i = M * (i,j) ) ) );