for z being Complex
for D being non empty set
for d1 being Element of D
for A being BinOp of D
for M being Function of [:COMPLEX,D:],D
for V being ComplexLinearSpace
for V1 being Subset of V
for v being VECTOR of V
for w being VECTOR of CLSStruct(# D,d1,A,M #) st V1 = D & M = the Mult of V | [:COMPLEX,V1:] & w = v holds
z * w = z * v by Lm4;