for R being domRing
for p being Polynomial of R
for a being non zero Element of R holds deg (a * p) = deg p