theorem :: E_TRANS1:17

for R being domRing
for f being Element of the carrier of (Polynom-Ring R) st len f > 1 & Char R = 0 holds
len ((Der1 R) . f) = (len f) - 1