let D be non empty set ; :: thesis: ( D is countable implies D * is countable )

defpred S_{1}[ 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_{1}[x,y]

A2: ( dom f = NAT & ( for x being object st x in NAT holds

S_{1}[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 *

defpred S

( $1 = n & $2 = n -tuples_on D );

A1: for x being object st x in NAT holds

ex y being object st S

proof

consider f being Function such that
let x be object ; :: thesis: ( x in NAT implies ex y being object st S_{1}[x,y] )

assume x in NAT ; :: thesis: ex y being object st S_{1}[x,y]

then reconsider n = x as Element of NAT ;

reconsider y = n -tuples_on D as set ;

take y ; :: thesis: S_{1}[x,y]

take n ; :: thesis: ( x = n & y = n -tuples_on D )

thus ( x = n & y = n -tuples_on D ) ; :: thesis: verum

end;assume x in NAT ; :: thesis: ex y being object st S

then reconsider n = x as Element of NAT ;

reconsider y = n -tuples_on D as set ;

take y ; :: thesis: S

take n ; :: thesis: ( x = n & y = n -tuples_on D )

thus ( x = n & y = n -tuples_on D ) ; :: thesis: verum

A2: ( dom f = NAT & ( for x being object st x in NAT holds

S

A3: D * = union { (k -tuples_on D) where k is Nat : verum } by FINSEQ_2:108;

A4: Union f = D *

proof

assume A12:
D is countable
; :: thesis: D * is countable
thus
Union f c= D *
:: according to XBOOLE_0:def 10 :: thesis: D * c= 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;proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in D * or x in Union f )
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;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

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

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

f . x is countable

hence
D * is countable
by A2, A4, Th11; :: thesis: verumf . 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;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