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