let RNS be non empty 1-sorted ; :: thesis: for S being sequence of RNS st ex x being Element of RNS st rng S = {x} holds
for n being Element of NAT holds S . n = S . (n + 1)
let S be sequence of RNS; :: thesis: ( ex x being Element of RNS st rng S = {x} implies for n being Element of NAT holds S . n = S . (n + 1) )
given z being Element of RNS such that A1: rng S = {z} ; :: thesis: for n being Element of NAT holds S . n = S . (n + 1)
let n be Element of NAT ; :: thesis: S . n = S . (n + 1)
( n in NAT & n + 1 in NAT ) ;
then ( n in dom S & n + 1 in dom S ) by FUNCT_2:def 1;
then ( S . n in {z} & S . (n + 1) in {z} ) by A1, FUNCT_1:def 5;
then ( S . n = z & S . (n + 1) = z ) by TARSKI:def 1;
hence S . n = S . (n + 1) ; :: thesis: verum