:: deftheorem defines * ZMODUL08:def 5 :
for G being Field
for V being VectSp of G
for W being Subset of V
for a being Element of G holds a * W = { (a * u) where u is Vector of V : u in W } ;