theorem Th44: :: FINSEQ_3:46

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