theorem Th15: :: RINGDER1:15

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