let m, n be Nat; :: 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:79;
then m <= len (idseq n) by CARD_1:def 7;
hence m <= n by CARD_1:def 7; :: 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 Th48; :: thesis: verum