:: deftheorem Def3 defines VectorSpace-Sequence VECTSP12:def 3 :
for K being Ring
for b₂ being non empty FinSequence holds
( b₂ is VectorSpace-Sequence of K iff for S being set st S in rng b₂ holds
S is VectSp of K );