:: deftheorem Def2 defines vector-distributive CLVECT_1:def 2 :
for IT being non empty CLSStruct holds
( IT is vector-distributive iff for a being Complex
for v, w being VECTOR of IT holds a * (v + w) = (a * v) + (a * w) );