theorem :: NORMSP_1:18

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