:: deftheorem defines * VECTSP_1:def 11 :
for F being non empty 1-sorted
for V being non empty ModuleStr over F
for x being Element of F
for v being Element of V holds x * v = the lmult of V . (x,v);