:: deftheorem Def9 defines * CONVEX4:def 9 :
for V being non empty CLSStruct
for a being Complex
for L, b₄ being C_Linear_Combination of V holds
( b₄ = a * L iff for v being VECTOR of V holds b₄ . v = a * (L . v) );