:: deftheorem Def7 defines In_Power BINOM:def 7 :
for R being non empty unital doubleLoopStr
for a, b being Element of R
for n being Nat
for b₅ being FinSequence of the carrier of R 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) ) ) );