len (idseq n) = len (id (Seg n)) by FINSEQ_2:def 1;
hence len (idseq n) = n ; :: thesis: verum