:: deftheorem Def14 defines scalar-distributive VECTSP_1:def 14 :
for F being non empty doubleLoopStr
for IT being non empty ModuleStr over F holds
( IT is scalar-distributive iff for x, y being Element of F
for v being Element of IT holds (x + y) * v = (x * v) + (y * v) );