theorem degpoly: :: RING_5:22

for R being domRing
for p being non zero Polynomial of R holds card (Roots p) <= deg p