theorem Th29: :: RINGDER1:29

for R being domRing
for f being Element of the carrier of (Polynom-Ring R)
for a being Element of R st f = anpoly (a,0) holds
(Der1 R) . f = 0_. R