:: deftheorem Def9 defines BiMod-like VECTSP_2:def 9 :
for R1, R2 being Ring
for IT being non empty BiModStr over R1,R2 holds
( IT is BiMod-like iff for x being Scalar of R1
for p being Scalar of R2
for v being Vector of IT holds x * (v * p) = (x * v) * p );