:: deftheorem Def6 defines scalar-distributive RLVECT_1:def 6 :
for IT being non empty RLSStruct holds
( IT is scalar-distributive iff for a, b being Real
for v being VECTOR of IT holds (a + b) * v = (a * v) + (b * v) );