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 S1[ 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 S1[m] holds
S1[m + 1]
proof
A3: k = rng f by ;
let m be Nat; :: thesis: ( S1[m] implies S1[m + 1] )
assume A4: S1[m] ; :: thesis: S1[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 ;
then A6: m in rng f by ;
A7: m < m + 1 by NAT_1:19;
m + 1 in rng f by ;
then min* (f " {m}) < min* (f " {(m + 1)}) by A1, A6, A7;
then m < min* (f " {(m + 1)}) by ;
hence m + 1 <= min* (f " {(m + 1)}) by NAT_1:13; :: thesis: verum
end;
A8: S1[ 0 ] ;
for m being Nat holds S1[m] from NAT_1:sch 2(A8, A2);
hence for m being Nat st m < k holds
m <= min* (f " {m}) ; :: thesis: verum