theorem Th8: :: RINGDER1:8

for R being non degenerated comRing
for n being Nat
for D being Derivation of R holds
( D |^ (n + 1) = D * (D |^ n) & dom D = the carrier of R & dom (D |^ n) = the carrier of R & D |^ n is the carrier of b₁ -valued Function )