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

( 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