theorem :: RINGDER1:10

for R being non degenerated comRing
for D being Derivation of R
for x, y, z being Element of R st z * y = 1. R holds
(y |^ 2) * (D . (x * z)) = (y * (D . x)) - (x * (D . y))