:: deftheorem Def13 defines vector-distributive VECTSP_1:def 13 :
for F being non empty doubleLoopStr
for IT being non empty ModuleStr over F holds
( IT is vector-distributive iff for x being Element of F
for v, w being Element of IT holds x * (v + w) = (x * v) + (x * w) );