:: deftheorem Def1 defines + BINOM:def 1 :
for R being non empty addLoopStr
for p, q, b₄ being FinSequence of the carrier of R holds
( b₄ = p + q iff ( dom b₄ = dom p & ( for i being Nat st 1 <= i & i <= len b₄ holds
b₄ /. i = (p /. i) + (q /. i) ) ) );