theorem :: FINSEQ_1:60

for n, i, m being Nat st i in Seg n holds
i + m in Seg (n + m)