theorem Th35: :: RINGDER1:35

for R being domRing
for x, y being Element of the carrier of (Polynom-Ring R) st not x is constant holds
(Der1 R) . (x * y) = (((Der1 R) . x) * y) + (x * ((Der1 R) . y))