theorem Th9: :: RINGDER1:9

for R being non degenerated comRing
for D being Derivation of R
for n being Nat
for x being Element of R holds (D |^ (n + 1)) . x = D . ((D |^ n) . x)