theorem Th46: :: FINSEQ_3:48

for k being Nat holds Sgm (Seg k) = idseq k