theorem BBD: :: FIELD_15:11

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