now :: thesis: not for v being Element of V holds v = 0. V

assume A: for v being Element of V holds v = 0. V ; :: thesis: contradiction

B: now :: thesis: for o being object st o in the carrier of V holds
o in {(0. V)}

let o be object ; :: thesis: ( o in the carrier of V implies o in {(0. V)} )
assume o in the carrier of V ; :: thesis: o in {(0. V)}
then o = 0. V by A;
hence o in {(0. V)} by TARSKI:def 1; :: thesis: verum

end;

for o being object st o in {(0. V)} holds
o in the carrier of V ;
hence contradiction by B, TARSKI:2; :: thesis: verum

end;

then consider v being Element of V such that
A: v <> 0. V ;
take {v} ; :: thesis: ( not {v} is empty & {v} is finite & {v} is linearly-independent )
thus ( not {v} is empty & {v} is finite & {v} is linearly-independent ) by A, VECTSP_7:3; :: thesis: verum