for n being Nat
for K being commutative Ring
for p being Element of Permutations n
for A being Matrix of n,K st n >= 1 holds
(Path_product (A @)) . (p ") = (Path_product A) . p