let A be set ; :: thesis: for i being Nat holds i -tuples_on A c= A *
let i be Nat; :: thesis: i -tuples_on A c= A *
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in i -tuples_on A or x in A * )
assume x in i -tuples_on A ; :: thesis: x in A *
then x is FinSequence of A by Def3;
hence x in A * by FINSEQ_1:def 11; :: thesis: verum