( k in NAT & dom (idseq k) = Seg k ) by ORDINAL1:def 12, RELAT_1:45;
hence len (idseq k) = k by FINSEQ_1:def 3; :: according to CARD_1:def 7 :: thesis: verum