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

proof

let x be object ; :: thesis: ( x in NAT implies ex y being object st S₁[x,y] )
assume x in NAT ; :: thesis: ex y being object 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 object st x in NAT holds
S₁[x,f . x] ) ) from CLASSES1:sch 1(A1);
A3: D * = union { (k -tuples_on D) where k is Nat : verum } by FINSEQ_2:108;
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 object ; :: 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 object such that
A7: y in dom f and
A8: X = f . y by A6, FUNCT_1:def 3;
reconsider y = y as Element of NAT by A2, A7;
ex n being Nat st
( y = n & X = n -tuples_on D ) by A2, A8;
then X in { (k -tuples_on D) where k is Nat : verum } ;
hence x in D * by A3, A5, TARSKI:def 4; :: thesis: verum

end;

let x be object ; :: 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 Nat : verum } ) by A3, TARSKI:def 4;
consider n being Nat such that
A10: X = n -tuples_on D by A9;
A11: n in NAT by ORDINAL1:def 12;
then ex k being Nat st
( n = k & f . n = k -tuples_on D ) by A2;
then X in rng f by A2, A10, FUNCT_1:def 3, A11;
hence x in Union f by A9, TARSKI:def 4; :: thesis: verum

end;

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

now :: thesis: for x being set st x in dom f holds
f . x is countable

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 Nat st
( x = n & f . x = n -tuples_on D ) by A2;
hence f . x is countable by A12, Th10; :: thesis: verum

end;

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