theorem Th16: :: RINGDER1:16

for R being non degenerated comRing
for x, y being Element of R
for D being Derivation of R holds LBZ (D,1,x,y) = <*(y * (D . x)),(x * (D . y))*>