let RNS be non empty 1-sorted ; :: thesis: 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
let S be sequence of RNS; :: thesis: ( ( for n, m being Nat holds S . n = S . m ) implies ex x being Element of RNS st
for n being Nat holds S . n = x )
assume that
A1: for n, m being Nat holds S . n = S . m and
A2: for x being Element of RNS ex n being Nat st S . n <> x ; :: thesis: contradiction

now :: thesis: for n being Nat holds contradiction

let n be Nat; :: thesis: contradiction
set z = S . n;
consider k being Nat such that
A3: S . k <> S . n by A2;
thus contradiction by A1, A3; :: thesis: verum

end;

hence contradiction ; :: thesis: verum