theorem :: FINSEQ_2:108

for D being non empty set holds D * = union { (i -tuples_on D) where i is Nat : verum }