let f be sequence of NAT; :: thesis: ( ( for n being Nat holds f . (n + 1) <= f . n ) implies ex m being Nat st
for n being Nat st m <= n holds
f . n = f . m )
assume A1: for n being Nat holds f . (n + 1) <= f . n ; :: thesis: ex m being Nat st
for n being Nat st m <= n holds
f . n = f . m
A2: for m, k being Nat st m <= k holds
f . k <= f . m

proof

defpred S₁[ Nat] means for m being Nat st m <= $1 holds
f . $1 <= f . m;
A3: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A4: S₁[k] ; :: thesis: S₁[k + 1]

now :: thesis: for m being Nat st m <= k + 1 holds
f . (k + 1) <= f . m

let m be Nat; :: thesis: ( m <= k + 1 implies f . (k + 1) <= f . b₁ )
assume A5: m <= k + 1 ; :: thesis: f . (k + 1) <= f . b₁

per cases ( m <= k or m = k + 1 ) by A5, NAT_1:8;

suppose A6: m <= k ; :: thesis: f . (k + 1) <= f . b₁

reconsider fk = f . k, fm = f . m, fk1 = f . (k + 1) as Nat ;
A7: fk1 <= fk by A1;
fk <= fm by A4, A6;
hence f . (k + 1) <= f . m by A7, XXREAL_0:2; :: thesis: verum

end;

suppose m = k + 1 ; :: thesis: f . (k + 1) <= f . b₁

hence f . (k + 1) <= f . m ; :: thesis: verum

end;

end;

end;

hence S₁[k + 1] ; :: thesis: verum

end;

A8: S₁[ 0 ] by XXREAL_0:1;
A9: for k being Nat holds S₁[k] from NAT_1:sch 2(A8, A3);
let m, k be Nat; :: thesis: ( m <= k implies f . k <= f . m )
assume m <= k ; :: thesis: f . k <= f . m
hence f . k <= f . m by A9; :: thesis: verum

end;

defpred S₁[ set ] means $1 in rng f;
A10: ex k being Nat st S₁[k]

proof

consider y being set such that
A11: y = f . 0 ;
reconsider k = y as Nat by A11;
take k ; :: thesis: S₁[k]
dom f = NAT by FUNCT_2:def 1;
hence S₁[k] by A11, FUNCT_1:def 3; :: thesis: verum

end;

ex k being Nat st
( S₁[k] & ( for n being Nat st S₁[n] holds
k <= n ) ) from NAT_1:sch 5(A10);
then consider l being Nat such that
A12: l in rng f and
A13: for n being Nat st n in rng f holds
l <= n ;
consider x being object such that
A14: x in dom f and
A15: l = f . x by A12, FUNCT_1:def 3;
reconsider m = x as Nat by A14;
A16: dom f = NAT by FUNCT_2:def 1;
for k being Nat st m <= k holds
f . k = f . m

proof

let k be Nat; :: thesis: ( m <= k implies f . k = f . m )
assume A17: m <= k ; :: thesis: f . k = f . m

now :: thesis: not f . k <> f . m

reconsider fk = f . k, fm = f . m as Nat ;
assume A18: f . k <> f . m ; :: thesis: contradiction
fk <= fm by A2, A17;
then A19: fk < fm by A18, XXREAL_0:1;
k in NAT by ORDINAL1:def 12;
then f . k in rng f by A16, FUNCT_1:def 3;
hence contradiction by A13, A15, A19; :: thesis: verum

end;

hence f . k = f . m ; :: thesis: verum

end;

hence ex m being Nat st
for n being Nat st m <= n holds
f . n = f . m ; :: thesis: verum