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

S_{1}[m + 1]
_{1}[ 0 ]
;

for m being Nat holds S_{1}[m]
from NAT_1:sch 2(A8, A2);

hence for m being Nat st m < k holds

m <= min* (f " {m}) ; :: thesis: verum

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 S

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 S

S

proof

A8:
S
A3:
k = rng f
by A1, FUNCT_2:def 3;

let m be Nat; :: thesis: ( S_{1}[m] implies S_{1}[m + 1] )

assume A4: S_{1}[m]
; :: thesis: S_{1}[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 A5, XXREAL_0:2;

then A6: m in rng f by A3, NAT_1:44;

A7: m < m + 1 by NAT_1:19;

m + 1 in rng f by A5, A3, NAT_1:44;

then min* (f " {m}) < min* (f " {(m + 1)}) by A1, A6, A7;

then m < min* (f " {(m + 1)}) by A4, A5, A7, XXREAL_0:2;

hence m + 1 <= min* (f " {(m + 1)}) by NAT_1:13; :: thesis: verum

end;let m be Nat; :: thesis: ( S

assume A4: S

assume A5: m + 1 < k ; :: thesis: m + 1 <= min* (f " {(m + 1)})

m < m + 1 by NAT_1:19;

then m < k by A5, XXREAL_0:2;

then A6: m in rng f by A3, NAT_1:44;

A7: m < m + 1 by NAT_1:19;

m + 1 in rng f by A5, A3, NAT_1:44;

then min* (f " {m}) < min* (f " {(m + 1)}) by A1, A6, A7;

then m < min* (f " {(m + 1)}) by A4, A5, A7, XXREAL_0:2;

hence m + 1 <= min* (f " {(m + 1)}) by NAT_1:13; :: thesis: verum

for m being Nat holds S

hence for m being Nat st m < k holds

m <= min* (f " {m}) ; :: thesis: verum