:: deftheorem Def2 defines Subnomial NEWTON04:def 2 :
for a, b being Real
for n being Nat
for b₄ being FinSequence of REAL holds
( b₄ = (a,b) Subnomial n iff ( len b₄ = n + 1 & ( for i, l, m being Nat st i in dom b₄ & m = i - 1 & l = n - m holds
b₄ . i = (a |^ l) * (b |^ m) ) ) );