for R being non degenerated comRing
for D being Derivation of R
for t being FinSequence of the carrier of R st len t >= 1 holds
Sum (DProd (D,t)) = D . (Product t)