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

defpred S₁[ Element of NAT ] means for m being Element of NAT st m <= $1 holds
f . $1 <= f . m;
A3: 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 A4: S₁[k] ; :: thesis: S₁[k + 1]

now

let m be Element of 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 Element of 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 ]

proof

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

end;

A10: for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A8, A3);
let m, k be Element of NAT ; :: thesis: ( m <= k implies f . k <= f . m )
assume m <= k ; :: thesis: f . k <= f . m
hence f . k <= f . m by A10; :: 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 ;
reconsider k = y as Element of NAT by A12;
take k ; :: thesis: S₁[k]
dom f = NAT by FUNCT_2:def 1;
hence S₁[k] by A12, 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(A11);
then consider l being Nat such that
A13: l in rng f and
A14: for n being Nat st n in rng f holds
l <= n ;
consider x being set such that
A15: x in dom f and
A16: l = f . x by A13, FUNCT_1:def 3;
reconsider m = x as Element of NAT by A15;
A17: dom f = NAT by 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 A18: m <= k ; :: thesis: f . k = f . m

now

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

end;

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

end;

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