theorem :: RINGDER1:25

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