theorem Th41: :: MATRIX11:41

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
the multF of K $$ (Path_matrix (p,(A * Perm))) = the multF of K $$ (Path_matrix (q,A))