theorem Th48: :: FINSEQ_3:50

for k, n being Nat holds (idseq (n + k)) | (Seg n) = idseq n