theorem Th24: :: E_TRANS1:24

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