theorem Th20: :: E_TRANS1:20

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
((Der1 INT.Ring) |^ k) . (f |^ k) = (k !) * (1. (Polynom-Ring INT.Ring))