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

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

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