theorem :: NORMSP_1:15

for RNS being non empty 1-sorted
for S being sequence of RNS st ex x being Element of RNS st rng S = {x} holds
for n being Nat holds S . n = S . (n + 1)