theorem Th6: :: RINGDER1:6
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 * x) = n * (D . x)