let k be natural number ; :: thesis: len (Sgm (Seg k)) = k
card (Seg k) = k by FINSEQ_1:78;
hence len (Sgm (Seg k)) = k by Th44; :: thesis: verum