for n being Nat
for K being commutative Ring
for A being Matrix of n,K
for p being Element of Permutations n
for Perm being Permutation of (Seg n)
for q being Element of Permutations n st q = p * (Perm ") holds
Path_matrix (p,(A * Perm)) = (Path_matrix (q,A)) * Perm