:: deftheorem Def9 defines poly_diff RINGDER1:def 9 :
for p being Polynomial of F_Real
for b₂ being sequence of F_Real holds
( b₂ = poly_diff p iff for n being Nat holds b₂ . n = (p . (n + 1)) * (n + 1) );