let k be Nat; :: thesis: len (idseq k) = k
reconsider k = k as Element of NAT by ORDINAL1:def 13;
dom (idseq k) = Seg k by RELAT_1:71;
hence len (idseq k) = k by FINSEQ_1:def 3; :: thesis: verum