let RNS be non empty 1-sorted ; :: thesis: for S being sequence of RNS st ( for n, m being Element of 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 Element of 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 Element of 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

let n be Element of NAT ; :: thesis: contradiction
consider z being Element of RNS such that
A3: S . n = z ;
consider k being Nat such that
A4: S . k <> z by A2;
k in NAT by ORDINAL1:def 12;
hence contradiction by A1, A3, A4; :: thesis: verum

end;

hence contradiction ; :: thesis: verum