for k, n being Nat holds Seg k c= Seg (k + n) by FINSEQ_1:5, NAT_1:12;