:: deftheorem Def5 defines vector-distributive RLVECT_1:def 5 :
for IT being non empty RLSStruct holds
( IT is vector-distributive iff for a being Real
for v, w being VECTOR of IT holds a * (v + w) = (a * v) + (a * w) );