theorem :: FIELD_14:62
for R being non degenerated comRing
for p being Element of the carrier of (Polynom-Ring R) holds (Deriv R) . (p |^ 0) = 0_. R