let i be natural Number ; :: thesis: idseq i is Element of i -tuples_on NAT
( idseq i is FinSequence of NAT & len (idseq i) = i ) by Th46, CARD_1:def 7;
hence idseq i is Element of i -tuples_on NAT by Th90; :: thesis: verum