theorem Th48: :: NUMBER19:48

for L being comRing
for z being FinSequence of the carrier of L
for f being NAT -valued FinSequence st len f = len z holds
for p being Permutation of (dom f)
for zp being FinSequence of the carrier of L st zp = z * p holds
Product (rpoly (f,z)) = Product (rpoly ((f * p),zp))