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 Th48, CARD_1:def 7;
hence idseq i is Element of i -tuples_on NAT by Th92; :: thesis: verum