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 )

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 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;

assume A1: for v being VECTOR of V st v in A holds
((- 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