:: deftheorem Def4 defines In_Power NEWTON:def 4 :
for a, b being Real
for n being natural Number
for b₄ being FinSequence of REAL holds
( b₄ = (a,b) In_Power 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 = ((n choose m) * (a |^ l)) * (b |^ m) ) ) );