:: deftheorem defines * RLVECT_1:def 1 :
for V being non empty RLSStruct
for v being VECTOR of V
for a being Real holds a * v = the Mult of V . (a,v);