theorem poly1: :: FIELD_8:2

for R being Ring
for p being Polynomial of R
for a being Element of R holds a * p = (a | R) *' p