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 A1: for i being Nat holds s . i = s . (i + 1) ; :: thesis: s is constant

now :: thesis: for i, j being Nat holds s . i = s . j

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

A2: now :: thesis: for i, j being Nat st i <= j holds
s . i = s . j

let i, j be Nat; :: thesis: ( i <= j implies s . i = s . j )
assume A3: i <= j ; :: thesis: s . i = s . j
defpred S₁[ Nat] means ( i <= $1 implies s . i = s . $1 );
A4: for j being Nat st S₁[j] holds
S₁[j + 1]

proof

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

end;

A6: S₁[ 0 ] by NAT_1:3;
for j being Nat holds S₁[j] from NAT_1:sch 2(A6, A4);
hence s . i = s . j by A3; :: thesis: verum

end;

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

end;

hence s is constant ; :: thesis: verum