:: deftheorem Def11 defines * RLVECT_2:def 11 :
for V being RealLinearSpace
for a being Real
for L, b₄ being Linear_Combination of V holds
( b₄ = a * L iff for v being VECTOR of V holds b₄ . v = a * (L . v) );