:: deftheorem defines product VECTSP12:def 5 :
for K being Ring
for G being VectorSpace-Sequence of K holds product G = ModuleStr(# (product (carr G)),[:(addop G):],(zeros G),[:(multop G):] #);