theorem Th25: :: RING_5:4
for R being domRing
for p being Polynomial of R
for a being non zero Element of R holds deg (a * p) = deg p