theorem :: RINGDER1:33

for R being domRing
for f, g being constant Element of the carrier of (Polynom-Ring R) holds (Der1 R) . (f * g) = (((Der1 R) . f) * g) + (f * ((Der1 R) . g))