theorem Th19: :: RINGDER1:19

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