let i be Nat; :: thesis: idseq i is Element of i -tuples_on NAT
( idseq i is FinSequence of NAT & len (idseq i) = i ) by Th52, FINSEQ_1:def 18;
hence idseq i is Element of i -tuples_on NAT by Th110; :: thesis: verum