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

proof

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

end;

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