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

proof

let m, k be Element of NAT ; :: thesis: ( m <= k implies f . k <= f . m )
assume A3: m <= k ; :: thesis: f . k <= f . m
defpred S₁[ Element of NAT ] means for m being Element of NAT st m <= $1 holds
f . $1 <= f . m;
A4: S₁[ 0 ]

proof

let m be Element of NAT ; :: thesis: ( m <= 0 implies f . 0 <= f . m )
assume A5: m <= 0 ; :: thesis: f . 0 <= f . m
0 <= m by NAT_1:2;
hence f . 0 <= f . m by A5, XXREAL_0:1; :: thesis: verum

end;

A6: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A7: S₁[k] ; :: thesis: S₁[k + 1]

now

let m be Element of NAT ; :: thesis: ( m <= k + 1 implies f . (k + 1) <= f . b₁ )
assume A8: m <= k + 1 ; :: thesis: f . (k + 1) <= f . b₁

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

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

reconsider fk = f . k, fm = f . m, fk1 = f . (k + 1) as Element of NAT ;
A10: fk <= fm by A7, A9;
fk1 <= fk by A1;
hence f . (k + 1) <= f . m by A10, 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;

for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A4, A6);
hence f . k <= f . m by A3; :: thesis: verum

end;

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

proof

consider y being set such that
A12: y = f . 0 ;
A13: dom f = NAT by FUNCT_2:def 1;
reconsider k = y as Element of NAT by A12;
take k ; :: thesis: S₁[k]
thus S₁[k] by A12, A13, FUNCT_1:def 5; :: 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(A11);
then consider l being Nat such that
A14: ( l in rng f & ( for n being Nat st n in rng f holds
l <= n ) ) ;
consider x being set such that
A15: ( x in dom f & l = f . x ) by A14, FUNCT_1:def 5;
A16: dom f = NAT by FUNCT_2:def 1;
reconsider m = x as Element of NAT by A15, FUNCT_2:def 1;
for k being Element of NAT st m <= k holds
f . k = f . m

proof

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

now

assume A18: f . k <> f . m ; :: thesis: contradiction
reconsider fk = f . k, fm = f . m as Element of NAT ;
fk <= fm by A2, A17;
then A19: fk < fm by A18, XXREAL_0:1;
f . k in rng f by A16, FUNCT_1:def 5;
hence contradiction by A14, A15, A19; :: thesis: verum

end;

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

end;

hence ex m being Element of NAT st
for k being Element of NAT st m <= k holds
f . k = f . m ; :: thesis: verum