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