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