:: deftheorem Def3 defines left-distributive VECTSP_1:def 3 :
for IT being non empty doubleLoopStr holds
( IT is left-distributive iff for a, b, c being Element of IT holds (b + c) * a = (b * a) + (c * a) );