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