theorem :: FINSEQ_1:61

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