let n, m be natural number ; :: thesis: ( (idseq n) | (Seg m) = idseq n iff n <= m )
len (idseq n) = n by FINSEQ_1:def 18;
hence ( (idseq n) | (Seg m) = idseq n iff n <= m ) by Th55; :: thesis: verum