theorem :: MATRIX_7:33

for n being Nat
for K being commutative Ring
for p being Element of Permutations n
for f, g being FinSequence of K st n >= 1 & len f = n & g = f * p holds
the multF of K $$ f = the multF of K $$ g by Th30, Th31;