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 * : ( 1 <= len x & 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 * : ( 1 <= len x & len x <= n ) } holds
X is finite
let X be set ; :: thesis: ( X = { x where x is Element of D * : ( 1 <= len x & len x <= n ) } implies X is finite )
deffunc H₁( Element of NAT ) -> FinSequenceSet of D = $1 -tuples_on D;
consider f being Function such that
A1: ( dom f = Seg n & ( for x being Element of NAT st x in Seg n holds
f . x = H₁(x) ) ) from CLASSES1:sch 2();
assume A2: X = { x where x is Element of D * : ( 1 <= len x & len x <= n ) } ; :: thesis: X is finite
A3: X c= Union f

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in Union f )
assume x in X ; :: thesis: x in Union f
then consider y being Element of D * such that
A4: x = y and
A5: ( 1 <= len y & len y <= n ) by A2;
consider m being Nat such that
A6: dom y = Seg m by FINSEQ_1:def 2;
m in NAT by ORDINAL1:def 12;
then A7: len y = m by A6, FINSEQ_1:def 3;
then A8: m in dom f by A1, A5, FINSEQ_1:1;
y in { s where s is Element of D * : len s = m } by A7;
then y in m -tuples_on D by FINSEQ_2:def 4;
then y in f . m by A1, A8;
hence x in Union f by A4, A8, CARD_5:2; :: thesis: verum

end;

now :: thesis: for x being object st x in dom f holds
f . x is finite

let x be object ; :: thesis: ( x in dom f implies f . x is finite )
assume A9: x in dom f ; :: thesis: f . x is finite
then reconsider z = x as Element of NAT by A1;
f . z = H₁(z) by A1, A9;
hence f . x is finite ; :: thesis: verum

end;

then Union f is finite by A1, CARD_2:88;
hence X is finite by A3; :: thesis: verum