:: deftheorem Def3 defines DProd RINGDER1:def 3 :
for R being non degenerated comRing
for D being Derivation of R
for s, b₄ being FinSequence of the carrier of R holds
( b₄ = DProd (D,s) iff ( len b₄ = len s & ( for i being Nat st i in dom b₄ holds
b₄ . i = Product (Replace (s,i,(D . (s /. i)))) ) ) );