theorem Th28: :: RINGDER1:28

for R being domRing
for f, g being Element of the carrier of (Polynom-Ring R)
for a being Element of R st f = a | R holds
(Der1 R) . (f * g) = (a | R) *' ((Der1 R) . g)