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 b1 -valued Function )