:: deftheorem Def5 defines Newton_Coeff NEWTON:def 5 :
for n being natural Number
for b₂ being FinSequence of REAL holds
( b₂ = Newton_Coeff n iff ( len b₂ = n + 1 & ( for i, k being Nat st i in dom b₂ & k = i - 1 holds
b₂ . i = n choose k ) ) );