let k, n be Element of NAT ; :: thesis: for f being Function of n,k st f is onto & f is "increasing holds
for m being Element of NAT st m < k holds
min* (f " {m}) <= (n - k) + m
let f be Function of n,k; :: thesis: ( f is onto & f is "increasing implies for m being Element of NAT st m < k holds
min* (f " {m}) <= (n - k) + m )
assume A1: ( f is onto & f is "increasing ) ; :: thesis: for m being Element of NAT st m < k holds
min* (f " {m}) <= (n - k) + m

now

per cases ( k = 0 or k > 0 ) ;

suppose k = 0 ; :: thesis: for m being Element of NAT st m < k holds
min* (f " {m}) <= (n - k) + m

hence for m being Element of NAT st m < k holds
min* (f " {m}) <= (n - k) + m ; :: thesis: verum

end;

suppose A2: k > 0 ; :: thesis: for m being Element of NAT st m < k holds
min* (f " {m}) <= (n - k) + m

defpred S₁[ Integer] means ( 0 <= $1 implies min* (f " {$1}) <= (n - k) + $1 );
reconsider k1 = k - 1 as Element of NAT by A2, NAT_1:20;
A3: ( 0 <= k1 & k1 < k1 + 1 ) by NAT_1:13;
A4: S₁[k1]

proof

assume 0 <= k1 ; :: thesis: min* (f " {k1}) <= (n - k) + k1
( k = 0 iff n = 0 ) by A1, Def1;
then min* (f " {k1}) <= n - 1 by Th16;
hence min* (f " {k1}) <= (n - k) + k1 ; :: thesis: verum

end;

A5: for m being Integer st m <= k1 & S₁[m] holds
S₁[m - 1]

proof

let m be Integer; :: thesis: ( m <= k1 & S₁[m] implies S₁[m - 1] )
assume A6: m <= k1 ; :: thesis: ( not S₁[m] or S₁[m - 1] )
assume A7: S₁[m] ; :: thesis: S₁[m - 1]
reconsider nk = n - k as Element of NAT by A1, Th17, NAT_1:21;
assume A8: 0 <= m - 1 ; :: thesis: min* (f " {(m - 1)}) <= (n - k) + (m - 1)
reconsider m1 = m - 1 as Element of NAT by A8, INT_1:16;
A9: ( m1 < m1 + 1 & m < k ) by A3, A6, NAT_1:19, XXREAL_0:2;
then m1 < k by XXREAL_0:2;
then ( m1 < k & m1 in k & m1 + 1 in k & k = rng f ) by A1, A9, FUNCT_2:def 3, NAT_1:45;
then ( min* (f " {m1}) < min* (f " {(m1 + 1)}) & min* (f " {(m1 + 1)}) <= (n - k) + m ) by A1, A7, A9, Def1;
then min* (f " {m1}) < (nk + m1) + 1 by XXREAL_0:2;
hence min* (f " {(m - 1)}) <= (n - k) + (m - 1) by NAT_1:13; :: thesis: verum

end;

A10: for m being Integer st m <= k1 holds
S₁[m] from INT_1:sch 3(A4, A5);

now

let m be Element of NAT ; :: thesis: ( m < k implies min* (f " {m}) <= (n - k) + m )
assume A11: m < k ; :: thesis: min* (f " {m}) <= (n - k) + m
m < k1 + 1 by A11;
then ( 0 <= m & m <= k1 ) by NAT_1:13;
hence min* (f " {m}) <= (n - k) + m by A10; :: thesis: verum

end;

hence for m being Element of NAT st m < k holds
min* (f " {m}) <= (n - k) + m ; :: thesis: verum

end;

end;

end;

hence for m being Element of NAT st m < k holds
min* (f " {m}) <= (n - k) + m ; :: thesis: verum