theorem Th20: :: RINGDER1:20

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