let k be Nat; :: thesis: len (Sgm (Seg k)) = k
card (Seg k) = k by FINSEQ_1:57;
hence len (Sgm (Seg k)) = k by Th37; :: thesis: verum