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 Th39; :: thesis: verum