:: deftheorem Def1 defines * RLVECT_X:def 1 :
for V being RealLinearSpace
for i being Integer
for L, b₄ being Linear_Combination of V holds
( b₄ = i * L iff for v being VECTOR of V holds b₄ . v = i * (L . v) );