theorem :: FIELD_6:8

for R being domRing
for p being non zero Polynomial of R holds deg (<%(0. R),(1. R)%> *' p) = (deg p) + 1