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 S1[ 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 & S1[m] holds
S1[m - 1]
proof
reconsider nk = n - k as Element of NAT by ;
A4: k = rng f by ;
let m be Integer; :: thesis: ( m <= k1 & S1[m] implies S1[m - 1] )
assume m <= k1 ; :: thesis: ( not S1[m] or S1[m - 1] )
then A5: m < k by ;
assume A6: S1[m] ; :: thesis: S1[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 ;
then A8: m1 in Segm k by NAT_1:44;
m1 + 1 in Segm k by ;
then min* (f " {m1}) < min* (f " {(m1 + 1)}) by A1, A7, A8, A4;
then min* (f " {m1}) < (nk + m1) + 1 by ;
hence min* (f " {(m - 1)}) <= (n - k) + (m - 1) by NAT_1:13; :: thesis: verum
end;
A9: S1[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
S1[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