theorem :: FIELD_15:12

for R being Ring
for p being Polynomial of R
for a, b being Element of R holds (a * b) * p = a * (b * p)