theorem :: NORMSP_1:17

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