:: deftheorem defines * ZMODUL02:def 1 :
for R being Ring
for V being LeftMod of R
for a being Element of R holds a * V = { (a * v) where v is Element of V : verum } ;