theorem Th49: :: FINSEQ_2:51

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