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