:: deftheorem Def11 defines addop PRVECT_1:def 12 :
for g being non empty non-empty-addLoopStr-yielding FinSequence
for b₂ being BinOps of carr g holds
( b₂ = addop g iff ( len b₂ = len (carr g) & ( for i being Element of dom (carr g) holds b₂ . i = the addF of (g . i) ) ) );