let D be non empty set ; :: thesis:
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]

let x be object ; :: thesis:
assume x in NAT ; :: thesis:
then reconsider n = x as Element of NAT ;
reconsider y = n -tuples_on D as set ;
take y ; :: thesis:
take n ; :: thesis:
thus ( x = n & y = n -tuples_on D ) ; :: thesis:

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 *

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

end;

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

end;

end;