let RNS be non empty 1-sorted ; :: thesis: for S being sequence of RNS st ex x being Element of RNS st
for n being Nat holds S . n = x holds
ex x being Element of RNS st rng S = {x}
let S be sequence of RNS; :: thesis: ( ex x being Element of RNS st
for n being Nat holds S . n = x implies ex x being Element of RNS st rng S = {x} )
given z being Element of RNS such that A1: for n being Nat holds S . n = z ; :: thesis: ex x being Element of RNS st rng S = {x}
take x = z; :: thesis: rng S = {x}

now

let t be set ; :: thesis: ( t in rng S implies t in {x} )
assume t in rng S ; :: thesis: t in {x}
then consider d being set such that
A2: d in dom S and
A3: S . d = t by FUNCT_1:def 5;
d in NAT by A2, FUNCT_2:def 1;
then t = z by A1, A3;
hence t in {x} by TARSKI:def 1; :: thesis: verum

end;

then A4: rng S c= {x} by TARSKI:def 3;

now

let s be set ; :: thesis: ( s in {x} implies s in rng S )
assume s in {x} ; :: thesis: s in rng S
then A5: s = x by TARSKI:def 1;

now

assume A6: not s in rng S ; :: thesis: contradiction

now

let n be Element of NAT ; :: thesis: contradiction
n in NAT ;
then n in dom S by FUNCT_2:def 1;
then S . n <> x by A5, A6, FUNCT_1:def 5;
hence contradiction by A1; :: thesis: verum

end;

hence contradiction ; :: thesis: verum

end;

hence s in rng S ; :: thesis: verum

end;

then {x} c= rng S by TARSKI:def 3;
hence rng S = {x} by A4, XBOOLE_0:def 10; :: thesis: verum