theorem LmA: :: RVSUM_4:14

for n, k being Nat st k in Segm (n + 1) holds
n - k is Nat