let D be non empty set ; :: thesis: ( D is countable implies D * is countable )
defpred S₁[ set , set ] means ex n being Element of NAT st
( $1 = n & $2 = n -tuples_on D );
A1: for x being set st x in NAT holds
ex y being set st S₁[x,y]

proof

let x be set ; :: thesis: ( x in NAT implies ex y being set st S₁[x,y] )
assume x in NAT ; :: thesis: ex y being set st S₁[x,y]
then reconsider n = x as Element of NAT ;
reconsider y = n -tuples_on D as set ;
take y ; :: thesis: S₁[x,y]
take n ; :: thesis: ( x = n & y = n -tuples_on D )
thus ( x = n & y = n -tuples_on D ) ; :: thesis: verum

end;

consider f being Function such that
A2: ( dom f = NAT & ( for x being set st x in NAT holds
S₁[x,f . x] ) ) from CLASSES1:sch 1(A1);
A3: D * = union { (k -tuples_on D) where k is Element of NAT : verum } by FINSEQ_2:128;
A4: Union f = D *

proof

thus Union f c= D * :: according to XBOOLE_0:def 10 :: thesis: D * c= Union f

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Union f or x in D * )
assume x in Union f ; :: thesis: x in D *
then consider X being set such that
A5: x in X and
A6: X in rng f by TARSKI:def 4;
consider y being set such that
A7: y in dom f and
A8: X = f . y by A6, FUNCT_1:def 5;
reconsider y = y as Element of NAT by A2, A7;
ex n being Element of NAT st
( y = n & X = n -tuples_on D ) by A2, A8;
then X in { (k -tuples_on D) where k is Element of NAT : verum } ;
hence x in D * by A3, A5, TARSKI:def 4; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in D * or x in Union f )
assume x in D * ; :: thesis: x in Union f
then consider X being set such that
A9: ( x in X & X in { (k -tuples_on D) where k is Element of NAT : verum } ) by A3, TARSKI:def 4;
consider n being Element of NAT such that
A10: X = n -tuples_on D by A9;
ex k being Element of NAT st
( n = k & f . n = k -tuples_on D ) by A2;
then X in rng f by A2, A10, FUNCT_1:def 5;
hence x in Union f by A9, TARSKI:def 4; :: thesis: verum

end;

assume A11: D is countable ; :: thesis: D * is countable

now

let x be set ; :: thesis: ( x in dom f implies f . x is countable )
assume x in dom f ; :: thesis: f . x is countable
then ex n being Element of NAT st
( x = n & f . x = n -tuples_on D ) by A2;
hence f . x is countable by A11, Th58; :: thesis: verum

end;

hence D * is countable by A2, A4, Th61; :: thesis: verum