let V be RealLinearSpace; :: thesis: for A being Subset of V holds
( A is affinely-independent iff for L being Linear_Combination of A st Sum L = 0. V & sum L = 0 holds
Carrier L = {} )
let A be Subset of V; :: thesis: ( A is affinely-independent iff for L being Linear_Combination of A st Sum L = 0. V & sum L = 0 holds
Carrier L = {} )
thus ( A is affinely-independent implies for L being Linear_Combination of A st Sum L = 0. V & sum L = 0 holds
Carrier L = {} ) by Lm5; :: thesis: ( ( for L being Linear_Combination of A st Sum L = 0. V & sum L = 0 holds
Carrier L = {} ) implies A is affinely-independent )
assume for L being Linear_Combination of A st Sum L = 0. V & sum L = 0 holds
Carrier L = {} ; :: thesis: A is affinely-independent
then for p being VECTOR of V st p in A holds
((- p) + A) \ {(0. V)} is linearly-independent by Lm6;
hence A is affinely-independent by Th41; :: thesis: verum