theorem Th18: :: FINSEQ_3:18

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