let D be non empty set ; :: thesis: D * = union { (i -tuples_on D) where i is Nat : verum }
for a being object holds
( a in D * iff a in union { (i -tuples_on D) where i is Nat : verum } )

proof

let a be object ; :: thesis: ( a in D * iff a in union { (i -tuples_on D) where i is Nat : verum } )
thus ( a in D * implies a in union { (i -tuples_on D) where i is Nat : verum } ) :: thesis: ( a in union { (i -tuples_on D) where i is Nat : verum } implies a in D * )

proof

assume a in D * ; :: thesis: a in union { (i -tuples_on D) where i is Nat : verum }
then reconsider a = a as FinSequence of D by FINSEQ_1:def 11;
( a is Element of (len a) -tuples_on D & (len a) -tuples_on D in { (i -tuples_on D) where i is Nat : verum } ) by Th90;
hence a in union { (i -tuples_on D) where i is Nat : verum } by TARSKI:def 4; :: thesis: verum

end;

assume a in union { (i -tuples_on D) where i is Nat : verum } ; :: thesis: a in D *
then consider Z being set such that
A1: a in Z and
A2: Z in { (i -tuples_on D) where i is Nat : verum } by TARSKI:def 4;
consider i being Nat such that
A3: Z = i -tuples_on D by A2;
ex s being Element of D * st
( s = a & len s = i ) by A1, A3;
hence a in D * ; :: thesis: verum

end;

hence D * = union { (i -tuples_on D) where i is Nat : verum } by TARSKI:2; :: thesis: verum