theorem :: NORMSP_1:16

for RNS being non empty 1-sorted
for S being sequence of RNS st ( for n being Nat holds S . n = S . (n + 1) ) holds
for n, k being Nat holds S . n = S . (n + k)