let k, n be natural number ; :: thesis: Seg k c= Seg (k + n)
k <= k + n by NAT_1:12;
hence Seg k c= Seg (k + n) by FINSEQ_1:7; :: thesis: verum