for i being natural Number holds idseq (i + 1) = (idseq i) ^ <*(i + 1)*>