:: deftheorem Def3 defines scalar-distributive CLVECT_1:def 3 :
for IT being non empty CLSStruct holds
( IT is scalar-distributive iff for a, b being Complex
for v being VECTOR of IT holds (a + b) * v = (a * v) + (b * v) );