:: deftheorem defines idseq FINSEQ_2:def 1 :
for i being natural Number holds idseq i = id (Seg i);