:: deftheorem defines (*) ZMODUL02:def 5 :
for R being commutative Ring
for V being LeftMod of R
for a being Element of R holds a (*) V = ModuleStr(# (a * V),(Add_ (a,V)),(Zero_ (a,V)),(Mult_ (a,V)) #);