let V be RealLinearSpace; :: thesis: for A being Subset of V holds

( A is affinely-independent iff for v being VECTOR of V st v in A holds

((- v) + A) \ {(0. V)} is linearly-independent )

let A be Subset of V; :: thesis: ( A is affinely-independent iff for v being VECTOR of V st v in A holds

((- v) + A) \ {(0. V)} is linearly-independent )

((- v) + A) \ {(0. V)} is linearly-independent ; :: thesis: A is affinely-independent

assume not A is empty ; :: according to RLAFFIN1:def 4 :: thesis: ex v being VECTOR of V st

( v in A & ((- v) + A) \ {(0. V)} is linearly-independent )

then consider v being object such that

A2: v in A ;

reconsider v = v as Element of V by A2;

take v ; :: thesis: ( v in A & ((- v) + A) \ {(0. V)} is linearly-independent )

thus ( v in A & ((- v) + A) \ {(0. V)} is linearly-independent ) by A1, A2; :: thesis: verum

( A is affinely-independent iff for v being VECTOR of V st v in A holds

((- v) + A) \ {(0. V)} is linearly-independent )

let A be Subset of V; :: thesis: ( A is affinely-independent iff for v being VECTOR of V st v in A holds

((- v) + A) \ {(0. V)} is linearly-independent )

hereby :: thesis: ( ( for v being VECTOR of V st v in A holds

((- v) + A) \ {(0. V)} is linearly-independent ) implies A is affinely-independent )

assume A1:
for v being VECTOR of V st v in A holds ((- v) + A) \ {(0. V)} is linearly-independent ) implies A is affinely-independent )

assume
A is affinely-independent
; :: thesis: for v being VECTOR of V st v in A holds

((- v) + A) \ {(0. V)} is linearly-independent

then for L being Linear_Combination of A st Sum L = 0. V & sum L = 0 holds

Carrier L = {} by Lm5;

hence for v being VECTOR of V st v in A holds

((- v) + A) \ {(0. V)} is linearly-independent by Lm6; :: thesis: verum

end;((- v) + A) \ {(0. V)} is linearly-independent

then for L being Linear_Combination of A st Sum L = 0. V & sum L = 0 holds

Carrier L = {} by Lm5;

hence for v being VECTOR of V st v in A holds

((- v) + A) \ {(0. V)} is linearly-independent by Lm6; :: thesis: verum

((- v) + A) \ {(0. V)} is linearly-independent ; :: thesis: A is affinely-independent

assume not A is empty ; :: according to RLAFFIN1:def 4 :: thesis: ex v being VECTOR of V st

( v in A & ((- v) + A) \ {(0. V)} is linearly-independent )

then consider v being object such that

A2: v in A ;

reconsider v = v as Element of V by A2;

take v ; :: thesis: ( v in A & ((- v) + A) \ {(0. V)} is linearly-independent )

thus ( v in A & ((- v) + A) \ {(0. V)} is linearly-independent ) by A1, A2; :: thesis: verum