theorem :: FINSEQ_2:111

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