theorem Th30: :: RINGDER1:30

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,1) holds
(Der1 R) . f = anpoly (a,0)