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