set A = { v where v is Vector of V : L . v <> 0. R } ;
consider T being finite Subset of V such that
A1: for v being Vector of V st not v in T holds
L . v = 0. R by Def2;
{ v where v is Vector of V : L . v <> 0. R } c= T

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { v where v is Vector of V : L . v <> 0. R } or x in T )
assume x in { v where v is Vector of V : L . v <> 0. R } ; :: thesis: x in T
then ex v being Vector of V st
( x = v & L . v <> 0. R ) ;
hence x in T by A1; :: thesis: verum

end;

hence { v where v is Vector of V : L . v <> 0. R } is finite Subset of V by XBOOLE_1:1; :: thesis: verum