:: deftheorem Def14 defines LinComb RLVECT_2:def 14 :
for V being RealLinearSpace
for b₂ being set holds
( b₂ = LinComb V iff for x being set holds
( x in b₂ iff x is Linear_Combination of V ) );