theorem :: FIELD_9:11

for R being non degenerated Ring
for p being non zero Polynomial of R
for q being Polynomial of R holds deg (p *' q) <= (deg p) + (deg q)