:: deftheorem Def8 defines multop PRVECT_2:def 8 :
for G being RealLinearSpace-Sequence
for b₂ being MultOps of REAL , carr G holds
( b₂ = multop G iff ( len b₂ = len (carr G) & ( for j being Element of dom (carr G) holds b₂ . j = the Mult of (G . j) ) ) );