theorem Th24: :: RINGDER1:24

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