:: deftheorem defines Mult_ ZMODUL02:def 4 :
for R being commutative Ring
for V being VectSp of R
for a being Element of R holds Mult_ (a,V) = the lmult of V | [: the carrier of R,(a * V):];