( k in NAT & dom (idseq k) = Seg k ) by ORDINAL1:def 13, RELAT_1:71;
hence len (idseq k) = k by FINSEQ_1:def 3; :: according to FINSEQ_1:def 18 :: thesis: verum