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

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