let k, n be Nat; :: thesis: for f being Function of (Segm n),(Segm k) st f is onto & f is "increasing holds
for m being Nat st m < k holds
m <= min* (f " {m})
let f be Function of (Segm n),(Segm k); :: thesis: ( f is onto & f is "increasing implies for m being Nat st m < k holds
m <= min* (f " {m}) )
defpred S₁[ Nat] means ( $1 < k implies $1 <= min* (f " {$1}) );
assume A1: ( f is onto & f is "increasing ) ; :: thesis: for m being Nat st m < k holds
m <= min* (f " {m})
A2: for m being Nat st S₁[m] holds
S₁[m + 1]

proof

A3: k = rng f by A1, FUNCT_2:def 3;
let m be Nat; :: thesis: ( S₁[m] implies S₁[m + 1] )
assume A4: S₁[m] ; :: thesis: S₁[m + 1]
assume A5: m + 1 < k ; :: thesis: m + 1 <= min* (f " {(m + 1)})
m < m + 1 by NAT_1:19;
then m < k by A5, XXREAL_0:2;
then A6: m in rng f by A3, NAT_1:44;
A7: m < m + 1 by NAT_1:19;
m + 1 in rng f by A5, A3, NAT_1:44;
then min* (f " {m}) < min* (f " {(m + 1)}) by A1, A6, A7;
then m < min* (f " {(m + 1)}) by A4, A5, A7, XXREAL_0:2;
hence m + 1 <= min* (f " {(m + 1)}) by NAT_1:13; :: thesis: verum

end;

A8: S₁[ 0 ] ;
for m being Nat holds S₁[m] from NAT_1:sch 2(A8, A2);
hence for m being Nat st m < k holds
m <= min* (f " {m}) ; :: thesis: verum