:: deftheorem Def5 defines addop PRVECT_2:def 5 :
for G being RealLinearSpace-Sequence
for b₂ being BinOps of carr G holds
( b₂ = addop G iff ( len b₂ = len (carr G) & ( for j being Element of dom (carr G) holds b₂ . j = the addF of (G . j) ) ) );