set A = Carrier L;

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 Def3;

Carrier L 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 by Def3;

Carrier L c= T

proof

hence
Carrier L is finite
; :: thesis: verum
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Carrier L or x in T )

assume x in Carrier L ; :: 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;assume x in Carrier L ; :: 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