let D be finite set ; :: thesis:
let n be Element of NAT ; :: thesis:
let X be set ; :: thesis:
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:
A3: X c= Union f

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in X ; :: thesis:
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:

end;

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

end;