:: deftheorem Def8 defines Der1 RINGDER1:def 8 :
for R being Ring
for b₂ being Function of (Polynom-Ring R),(Polynom-Ring R) holds
( b₂ = Der1 R iff for f being Element of the carrier of (Polynom-Ring R)
for i being Nat holds (b₂ . f) . i = (i + 1) * (f . (i + 1)) );