theorem Th10: :: FIELD_1:9

for n being Nat
for R being non degenerated comRing
for a, b being non zero Element of R holds b * (anpoly (a,n)) = anpoly ((a * b),n)