:: deftheorem Def7 defines |-- RLAFFIN1:def 7 :
for V being RealLinearSpace
for A being Subset of V st A is affinely-independent holds
for x being object st x in Affin A holds
for b₄ being Linear_Combination of A holds
( b₄ = x |-- A iff ( Sum b₄ = x & sum b₄ = 1 ) );