:: deftheorem Def8 defines multop VECTSP12:def 4 :
for K being Ring
for G being VectorSpace-Sequence of K
for b₃ being MultOps of the carrier of K, carr G holds
( b₃ = multop G iff ( len b₃ = len (carr G) & ( for j being Element of dom (carr G) holds b₃ . j = the lmult of (G . j) ) ) );