theorem Th22: :: E_TRANS1:22

for R being domRing
for f being Element of the carrier of (Polynom-Ring R)
for k, i being Nat holds (((Der1 R) |^ k) . f) . i = (eta ((i + k),k)) * (f . (i + k))