set A = { v where v is Element of V : L . v <> 0 } ;
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 by Def5;
{ v where v is Element of V : L . v <> 0 } c= T

proof

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

end;

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