let V be RealLinearSpace; :: thesis:
let v be VECTOR of V; :: thesis:
thus ( {v} is linearly-independent implies v <> 0. V ) :: thesis:

proof

assume {v} is linearly-independent ; :: thesis:
then not 0. V in {v} by Th6;
hence v <> 0. V by TARSKI:def 1; :: thesis:

end;

assume A1: v <> 0. V ; :: thesis:
let l be Linear_Combination of {v}; :: according to RLVECT_3:def 1 :: thesis:
A2: Carrier l c= {v} by RLVECT_2:def 6;
assume A3: Sum l = 0. V ; :: thesis:

now :: thesis:

per cases by A2, ZFMISC_1:33;

suppose Carrier l = {} ; :: thesis:

hence Carrier l = {} ; :: thesis:

end;

suppose A4: Carrier l = {v} ; :: thesis:

A5: 0. V = (l . v) * v by A3, RLVECT_2:32;

now :: thesis:

assume v in Carrier l ; :: thesis:
then ex u being VECTOR of V st
( v = u & l . u <> 0 ) ;
hence contradiction by A1, A5, RLVECT_1:11; :: thesis:

end;

hence Carrier l = {} by A4, TARSKI:def 1; :: thesis:

end;

end;

end;

hence Carrier l = {} ; :: thesis: