let D be finite set ; :: thesis: for n being Element of NAT
for X being set st X = { x where x is Element of D * : len x <= n } holds
X is finite
let n be Element of NAT ; :: thesis: for X being set st X = { x where x is Element of D * : len x <= n } holds
X is finite
let X be set ; :: thesis: ( X = { x where x is Element of D * : len x <= n } implies X is finite )
set B = { x where x is Element of D * : ( 1 <= len x & len x <= n ) } ;
assume A1: X = { x where x is Element of D * : len x <= n } ; :: thesis: X is finite
A2: X c= {{}} \/ { x where x is Element of D * : ( 1 <= len x & len x <= n ) }

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in X or y in {{}} \/ { x where x is Element of D * : ( 1 <= len x & len x <= n ) } )
assume y in X ; :: thesis: y in {{}} \/ { x where x is Element of D * : ( 1 <= len x & len x <= n ) }
then consider x being Element of D * such that
A3: y = x and
A4: len x <= n by A1;

per cases ( len x < 0 + 1 or len x >= 0 + 1 ) ;

suppose len x < 0 + 1 ; :: thesis: y in {{}} \/ { x where x is Element of D * : ( 1 <= len x & len x <= n ) }

then x = {} by NAT_1:13;
then x in {{}} by TARSKI:def 1;
hence y in {{}} \/ { x where x is Element of D * : ( 1 <= len x & len x <= n ) } by A3, XBOOLE_0:def 3; :: thesis: verum

end;

suppose len x >= 0 + 1 ; :: thesis: y in {{}} \/ { x where x is Element of D * : ( 1 <= len x & len x <= n ) }

then x in { x where x is Element of D * : ( 1 <= len x & len x <= n ) } by A4;
hence y in {{}} \/ { x where x is Element of D * : ( 1 <= len x & len x <= n ) } by A3, XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

{ x where x is Element of D * : ( 1 <= len x & len x <= n ) } is finite by Th2;
hence X is finite by A2; :: thesis: verum