let X be non empty set ; :: thesis: for s being sequence of X st ( for i being Nat holds s . i = s . (i + 1) ) holds
s is constant
let s be sequence of X; :: thesis: ( ( for i being Nat holds s . i = s . (i + 1) ) implies s is constant )
assume Z: for i being Nat holds s . i = s . (i + 1) ; :: thesis: s is constant

now

let i, j be Nat; :: thesis: s . i = s . j

L: now

let i, j be Nat; :: thesis: ( i <= j implies s . i = s . j )
assume zz: i <= j ; :: thesis: s . i = s . j
defpred S₁[ Nat] means ( i <= $1 implies s . i = s . $1 );
( i <= 0 implies i = 0 ) by NAT_1:3;
then A: S₁[ 0 ] ;
B: for j being Nat st S₁[j] holds
S₁[j + 1]

proof

let j be Nat; :: thesis: ( S₁[j] implies S₁[j + 1] )
assume z: S₁[j] ; :: thesis: S₁[j + 1]
assume i <= j + 1 ; :: thesis: s . i = s . (j + 1)
then C: ( i < j + 1 or i = j + 1 ) by XXREAL_0:1;
s . j = s . (j + 1) by Z;
hence s . i = s . (j + 1) by C, z, NAT_1:13; :: thesis: verum

end;

for j being Nat holds S₁[j] from NAT_1:sch 2(A, B);
hence s . i = s . j by zz; :: thesis: verum

end;

( i <= j or j <= i ) ;
hence s . i = s . j by L; :: thesis: verum

end;

hence s is constant by Th24; :: thesis: verum