theorem Th31: :: MATRIX_7:32

for n being Nat
for K being commutative Ring
for p being Element of Permutations n
for f, g being FinSequence of K st len f = n & g = f * p holds
f,g are_fiberwise_equipotent