let n, m be natural number ; :: thesis: ( (idseq n) | (Seg m) = idseq m iff m <= n )
thus ( (idseq n) | (Seg m) = idseq m implies m <= n ) :: thesis: ( m <= n implies (idseq n) | (Seg m) = idseq m )

proof

assume (idseq n) | (Seg m) = idseq m ; :: thesis: m <= n
then len (idseq m) <= len (idseq n) by FINSEQ_1:100;
then m <= len (idseq n) by FINSEQ_1:def 18;
hence m <= n by FINSEQ_1:def 18; :: thesis: verum

end;

assume m <= n ; :: thesis: (idseq n) | (Seg m) = idseq m
then ex j being Nat st n = m + j by NAT_1:10;
hence (idseq n) | (Seg m) = idseq m by Th56; :: thesis: verum