let X be non empty set ; :: thesis: ex f being Function st
( dom f = NAT & ( for n being Nat holds f . n = n -tuples_on X ) & union (rng f) = X * )
defpred S₁[ object , object ] means ex n being Nat st
( $1 = n & $2 = n -tuples_on X );
A1: for x, y1, y2 being object st x in NAT & S₁[x,y1] & S₁[x,y2] holds
y1 = y2 ;
A2: 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 z = x as Nat ;
take z -tuples_on X ; :: thesis: S₁[x,z -tuples_on X]
thus S₁[x,z -tuples_on X] ; :: thesis: verum

end;

consider f being Function such that
A3: dom f = NAT and
A4: for x being object st x in NAT holds
S₁[x,f . x] from FUNCT_1:sch 2(A1, A2);
A5: for n being Nat holds f . n = n -tuples_on X

proof

let n be Nat; :: thesis: f . n = n -tuples_on X
S₁[n,f . n] by A4, ORDINAL1:def 12;
hence f . n = n -tuples_on X ; :: thesis: verum

end;

union (rng f) = X *

proof

now :: thesis: ( union (rng f) c= X * & X * c= union (rng f) )

now :: thesis: for x being object st x in union (rng f) holds
x in X *

let x be object ; :: thesis: ( x in union (rng f) implies x in X * )
assume x in union (rng f) ; :: thesis: x in X *
then consider y being set such that
A6: x in y and
A7: y in rng f by TARSKI:def 4;
consider z being object such that
A8: z in dom f and
A9: y = f . z by A7, FUNCT_1:def 3;
reconsider z = z as Nat by A3, A8;
A10: x in z -tuples_on X by A5, A6, A9;
z -tuples_on X c= X * by FINSEQ_2:90;
hence x in X * by A10; :: thesis: verum

end;

hence union (rng f) c= X * ; :: thesis: X * c= union (rng f)

now :: thesis: for x being object st x in X * holds
x in union (rng f)

let x be object ; :: thesis: ( x in X * implies x in union (rng f) )
assume x in X * ; :: thesis: x in union (rng f)
then consider n being Nat such that
A11: x in n -tuples_on X by Th62;
n -tuples_on X in rng f

proof

A12: n in dom f by A3, ORDINAL1:def 12;
f . n = n -tuples_on X by A5;
hence n -tuples_on X in rng f by A12, FUNCT_1:def 3; :: thesis: verum

end;

hence x in union (rng f) by A11, TARSKI:def 4; :: thesis: verum

end;

hence X * c= union (rng f) ; :: thesis: verum

end;

hence union (rng f) = X * ; :: thesis: verum

end;

hence ex f being Function st
( dom f = NAT & ( for n being Nat holds f . n = n -tuples_on X ) & union (rng f) = X * ) by A3, A5; :: thesis: verum