:: deftheorem Def7 defines distributive VECTSP_1:def 7 :
for IT being non empty doubleLoopStr holds
( IT is distributive iff for x, y, z being Element of IT holds
( x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) ) );