:: deftheorem Def11 defines addop PRVECT_1:def 11 :
for g being Group-Sequence
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) ) ) );