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