for R being non degenerated comRing
for D being Derivation of R
for s being FinSequence of the carrier of R holds D . (Sum s) = Sum (D * s) by Th11;