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 = 0c by Def1;
now :: thesis: for x being object st x in Carrier L holds
x in T
let x be object ; :: thesis: ( x in Carrier L implies x in T )
assume x in Carrier L ; :: thesis: x in T
then ex v being Element of V st
( x = v & L . v <> 0c ) ;
hence x in T by A1; :: thesis: verum
end;
then Carrier L c= T ;
hence Carrier L is finite ; :: thesis: verum