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 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 Nat holds S . n = S . (n + 1) )
given z being Element of RNS such that A1: rng S = {z} ; :: thesis: for n being Nat holds S . n = S . (n + 1)
let n be Nat; :: thesis: S . n = S . (n + 1)
n in NAT by ORDINAL1:def 12;
then n in dom S by FUNCT_2:def 1;
then S . n in {z} by A1, FUNCT_1:def 3;
then A2: S . n = z by TARSKI:def 1;
n + 1 in NAT ;
then n + 1 in dom S by FUNCT_2:def 1;
then S . (n + 1) in {z} by A1, FUNCT_1:def 3;
hence S . n = S . (n + 1) by A2, TARSKI:def 1; :: thesis: verum