let A be non empty set ; :: thesis: for n being Nat holds n -tuples_on A c= A *
let n be Nat; :: thesis: n -tuples_on A c= A *
defpred S₁[ Element of A * ] means len $1 = n;
{ s where s is Element of A * : S₁[s] } c= A * from FRAENKEL:sch 10();
hence n -tuples_on A c= A * ; :: thesis: verum