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

min* (f " {m}) <= (n - k) + m ; :: thesis: verum

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) + mend;

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

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

end;

suppose
k > 0
; :: thesis: for m being Nat st m < k holds

min* (f " {m}) <= (n - k) + m

min* (f " {m}) <= (n - k) + m

then reconsider k1 = k - 1 as Element of NAT by NAT_1:20;

defpred S_{1}[ 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_{1}[m] holds

S_{1}[m - 1]
_{1}[k1]

S_{1}[m]
from INT_1:sch 3(A9, A3);

min* (f " {m}) <= (n - k) + m ; :: thesis: verum

end;defpred S

A2: k1 < k1 + 1 by NAT_1:13;

A3: for m being Integer st m <= k1 & S

S

proof

A9:
S
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_{1}[m] implies S_{1}[m - 1] )

assume m <= k1 ; :: thesis: ( not S_{1}[m] or S_{1}[m - 1] )

then A5: m < k by A2, XXREAL_0:2;

assume A6: S_{1}[m]
; :: thesis: S_{1}[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;A4: k = rng f by A1, FUNCT_2:def 3;

let m be Integer; :: thesis: ( m <= k1 & S

assume m <= k1 ; :: thesis: ( not S

then A5: m < k by A2, XXREAL_0:2;

assume A6: S

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

proof

A10:
for m being Integer st m <= k1 holds
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;( k = 0 iff n = 0 ) by A1;

then min* (f " {k1}) <= n - 1 by Th16;

hence min* (f " {k1}) <= (n - k) + k1 ; :: thesis: verum

S

now :: 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

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;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

min* (f " {m}) <= (n - k) + m ; :: thesis: verum

min* (f " {m}) <= (n - k) + m ; :: thesis: verum