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