:: deftheorem defines * CLVECT_1:def 1 :
for V being non empty CLSStruct
for v being VECTOR of V
for z being Complex holds z * v = the Mult of V . [z,v];