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
min* (f " {m}) <= (n - k) + 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
min* (f " {m}) <= (n - k) + m )
assume A1: ( f is onto & f is "increasing ) ; :: thesis: for m being Nat st m < k holds
min* (f " {m}) <= (n - k) + m

now :: thesis: for m being Nat st m < k holds
min* (f " {m}) <= (n - k) + m

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

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

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

end;

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

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

proof

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

end;

A9: S₁[k1]

proof

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

end;

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

now :: thesis: for m being Nat st m < k holds
min* (f " {m}) <= (n - k) + m

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

end;

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

end;

end;

end;

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