theorem Th18: :: RINGDER1:18

for R being non degenerated comRing
for m being Nat
for x, y being Element of R
for D being Derivation of R holds LBZ0 (D,m,x,y) = (LBZ1 (D,m,x,y)) + (LBZ2 (D,m,x,y))