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