:: deftheorem Def5 defines poly_diff POLYDIFF:def 5 :
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) );