:: deftheorem Def8 defines RightMod-like VECTSP_2:def 8 :
for R being non empty doubleLoopStr
for IT being non empty RightModStr over R holds
( IT is RightMod-like iff for x, y being Scalar of R
for v, w being Vector of IT holds
( (v + w) * x = (v * x) + (w * x) & v * (x + y) = (v * x) + (v * y) & v * (y * x) = (v * y) * x & v * (1_ R) = v ) );