theorem :: FINSEQ_3:47

for k, n being Nat holds (Sgm (Seg (k + n))) | (Seg k) = Sgm (Seg k) by Lm4;