theorem :: FINSEQ_1:61

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