theorem Th21: :: RINGDER1:21

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 (D * (LBZ0 (D,n,x,y))) = ((- ((LBZ1 (D,(n + 1),x,y)) /. 1)) + (Sum (LBZ0 (D,(n + 1),x,y)))) - ((LBZ2 (D,(n + 1),x,y)) /. (n + 1))