theorem Th22: :: RINGDER1:22

for R being non degenerated comRing
for n being Nat
for x, y being Element of R
for D being Derivation of R holds LBZ (D,(n + 1),x,y) = (<*(((D |^ (n + 1)) . x) * y)*> ^ (LBZ0 (D,n,x,y))) ^ <*(x * ((D |^ (n + 1)) . y))*>