theorem der3: :: FIELD_14:59

for R being Ring
for p being Element of the carrier of (Polynom-Ring R)
for a being Element of R holds (Deriv R) . (a * p) = a * ((Deriv R) . p)