theorem Th7: :: RINGDER1:7

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