theorem Th23: :: RINGDER1:23

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