theorem :: FINSEQ_2:49

for i being natural Number
for k being Element of Seg i holds (idseq i) . k = k ;