theorem Th87: :: NUMBER19:87
for n, k, d, s being Nat holds
( s in seq (n,k) iff s + d in seq ((n + d),k) )