for i being natural Number holds idseq i is Element of i -tuples_on NAT