theorem der4: :: FIELD_14:60

for R being non degenerated comRing
for p being constant Element of the carrier of (Polynom-Ring R) holds (Deriv R) . p = 0_. R