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 :: thesis: for s being object st s in {x} holds
s in rng S
let s be object ; :: thesis: ( s in {x} implies s in rng S )
assume s in {x} ; :: thesis: s in rng S
then A2: s = x by TARSKI:def 1;
now :: thesis: s in rng S
assume A3: not s in rng S ; :: thesis: contradiction
now :: thesis: for n being Nat holds contradiction
let n be Nat; :: thesis: contradiction
n in NAT by ORDINAL1:def 12;
then n in dom S by FUNCT_2:def 1;
then S . n <> x by A2, A3, FUNCT_1:def 3;
hence contradiction by A1; :: thesis: verum
end;
hence contradiction ; :: thesis: verum
end;
hence s in rng S ; :: thesis: verum
end;
then A4: {x} c= rng S by TARSKI:def 3;
now :: thesis: for t being object st t in rng S holds
t in {x}
let t be object ; :: thesis: ( t in rng S implies t in {x} )
assume t in rng S ; :: thesis: t in {x}
then consider d being object such that
A5: d in dom S and
A6: S . d = t by FUNCT_1:def 3;
d in NAT by A5, FUNCT_2:def 1;
then t = z by A1, A6;
hence t in {x} by TARSKI:def 1; :: thesis: verum
end;
then rng S c= {x} by TARSKI:def 3;
hence rng S = {x} by A4, XBOOLE_0:def 10; :: thesis: verum