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