theorem :: RINGDER1:17

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 (LBZ0 (D,n,x,y))) = Sum (D * (LBZ0 (D,n,x,y))) by Th11;