{v} is affinely-independent
_{1} being Subset of V st b_{1} = {v} holds

b_{1} is affinely-independent
; :: thesis: verum

proof

hence
for b
assume
not {v} is empty
; :: according to RLAFFIN1:def 4 :: thesis: ex v being VECTOR of V st

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

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

thus v in {v} by TARSKI:def 1; :: thesis: ((- v) + {v}) \ {(0. V)} is linearly-independent

(- v) + v = 0. V by RLVECT_1:5;

then (- v) + {v} = {(0. V)} by Lm3;

then ((- v) + {v}) \ {(0. V)} = {} the carrier of V by XBOOLE_1:37;

hence ((- v) + {v}) \ {(0. V)} is linearly-independent by RLVECT_3:7; :: thesis: verum

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

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

thus v in {v} by TARSKI:def 1; :: thesis: ((- v) + {v}) \ {(0. V)} is linearly-independent

(- v) + v = 0. V by RLVECT_1:5;

then (- v) + {v} = {(0. V)} by Lm3;

then ((- v) + {v}) \ {(0. V)} = {} the carrier of V by XBOOLE_1:37;

hence ((- v) + {v}) \ {(0. V)} is linearly-independent by RLVECT_3:7; :: thesis: verum

b