( n in NAT & dom (id (Seg n)) = Seg n ) by ORDINAL1:def 12;
hence len (id (Seg n)) = n by FINSEQ_1:def 3; :: thesis: verum