theorem Th19: :: E_TRANS1:19

for k being Nat
for f being Element of the carrier of (Polynom-Ring INT.Ring) st ((Der1 INT.Ring) |^ 1) . (f |^ 1) = 1. (Polynom-Ring INT.Ring) holds
for j being Nat st 1 <= j & j <= k holds
((Der1 INT.Ring) |^ j) . (f |^ k) = (eta (k,j)) * (f |^ (k -' j))