reconsider S = {(0. V)} as Subset of V ;
take S ; :: thesis: not S is linearly-independent
0. V in S by TARSKI:def 1;
hence not S is linearly-independent by VECTSP_7:2; :: thesis: verum