let k, n be Nat; :: thesis: not ( ( n = 0 implies k = 0 ) & ( k = 0 implies n = 0 ) & n >= k & ( for f being Function of (Segm n),(Segm k) holds

( not f is onto or not f is "increasing ) ) )

assume that

A1: ( n = 0 iff k = 0 ) and

A2: n >= k ; :: thesis: ex f being Function of (Segm n),(Segm k) st

( f is onto & f is "increasing )

( f is onto & f is "increasing ) ; :: thesis: verum

( not f is onto or not f is "increasing ) ) )

assume that

A1: ( n = 0 iff k = 0 ) and

A2: n >= k ; :: thesis: ex f being Function of (Segm n),(Segm k) st

( f is onto & f is "increasing )

now :: thesis: ex f being Function of (Segm n),(Segm k) st

( f is onto & f is "increasing )end;

hence
ex f being Function of (Segm n),(Segm k) st ( f is onto & f is "increasing )

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

end;

suppose A3:
n = 0
; :: thesis: ex f being Function of (Segm n),(Segm k) st

( f is onto & f is "increasing )

( f is onto & f is "increasing )

set f = {} ;

A4: dom {} = n by A3;

rng {} = k by A1, A3;

then reconsider f = {} as Function of (Segm n),(Segm k) by A4, FUNCT_2:1;

( f is onto & f is "increasing ) by A1, Th15;

hence ex f being Function of (Segm n),(Segm k) st

( f is onto & f is "increasing ) ; :: thesis: verum

end;A4: dom {} = n by A3;

rng {} = k by A1, A3;

then reconsider f = {} as Function of (Segm n),(Segm k) by A4, FUNCT_2:1;

( f is onto & f is "increasing ) by A1, Th15;

hence ex f being Function of (Segm n),(Segm k) st

( f is onto & f is "increasing ) ; :: thesis: verum

suppose A5:
n > 0
; :: thesis: ex f being Function of (Segm n),(Segm k) st

( f is onto & f is "increasing )

( f is onto & f is "increasing )

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

reconsider k = k, n = n as non zero Element of NAT by A1, A5, ORDINAL1:def 12;

defpred S_{1}[ Element of Segm n, Element of Segm k] means $2 = min ($1,k1);

A6: for x being Element of Segm n ex y being Element of Segm k st S_{1}[x,y]

A8: for m being Element of Segm n holds S_{1}[m,f . m]
from FUNCT_2:sch 3(A6);

then k = rng f ;

then A13: f is onto by FUNCT_2:def 3;

A14: for m being Nat st m in rng f holds

min* (f " {m}) = m

hence ex f being Function of (Segm n),(Segm k) st

( f is onto & f is "increasing ) by A13; :: thesis: verum

end;reconsider k = k, n = n as non zero Element of NAT by A1, A5, ORDINAL1:def 12;

defpred S

A6: for x being Element of Segm n ex y being Element of Segm k st S

proof

consider f being Function of (Segm n),(Segm k) such that
let x be Element of Segm n; :: thesis: ex y being Element of Segm k st S_{1}[x,y]

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

min (x,k1) <= k1 by XXREAL_0:17;

then min (x,k1) < k by A7, XXREAL_0:2;

then min (x,k1) in Segm k by NAT_1:44;

hence ex y being Element of Segm k st S_{1}[x,y]
; :: thesis: verum

end;A7: k1 < k1 + 1 by NAT_1:13;

min (x,k1) <= k1 by XXREAL_0:17;

then min (x,k1) < k by A7, XXREAL_0:2;

then min (x,k1) in Segm k by NAT_1:44;

hence ex y being Element of Segm k st S

A8: for m being Element of Segm n holds S

now :: thesis: for m9 being object st m9 in Segm k holds

m9 in rng f

then
k c= rng f
;m9 in rng f

let m9 be object ; :: thesis: ( m9 in Segm k implies m9 in rng f )

assume A9: m9 in Segm k ; :: thesis: m9 in rng f

reconsider m = m9 as Element of NAT by A9;

A10: m < k1 + 1 by A9, NAT_1:44;

then m < n by A2, XXREAL_0:2;

then A11: m in Segm n by NAT_1:44;

then A12: m in dom f by FUNCT_2:def 1;

m <= k1 by A10, NAT_1:13;

then min (m,k1) = m by XXREAL_0:def 9;

then f . m = m by A8, A11;

hence m9 in rng f by A12, FUNCT_1:def 3; :: thesis: verum

end;assume A9: m9 in Segm k ; :: thesis: m9 in rng f

reconsider m = m9 as Element of NAT by A9;

A10: m < k1 + 1 by A9, NAT_1:44;

then m < n by A2, XXREAL_0:2;

then A11: m in Segm n by NAT_1:44;

then A12: m in dom f by FUNCT_2:def 1;

m <= k1 by A10, NAT_1:13;

then min (m,k1) = m by XXREAL_0:def 9;

then f . m = m by A8, A11;

hence m9 in rng f by A12, FUNCT_1:def 3; :: thesis: verum

then k = rng f ;

then A13: f is onto by FUNCT_2:def 3;

A14: for m being Nat st m in rng f holds

min* (f " {m}) = m

proof

let m be Nat; :: thesis: ( m in rng f implies min* (f " {m}) = m )

assume m in rng f ; :: thesis: min* (f " {m}) = m

then A15: m < k1 + 1 by NAT_1:44;

then A16: m <= k1 by NAT_1:13;

m < n by A2, A15, XXREAL_0:2;

then A17: m in Segm n by NAT_1:44;

then A18: m in dom f by FUNCT_2:def 1;

m <= k1 by A15, NAT_1:13;

then min (m,k1) = m by XXREAL_0:def 9;

then f . m = m by A8, A17;

then A19: f . m in {m} by TARSKI:def 1;

then A20: m in f " {m} by A18, FUNCT_1:def 7;

A21: not f " {m} is empty by A19, A18, FUNCT_1:def 7;

end;assume m in rng f ; :: thesis: min* (f " {m}) = m

then A15: m < k1 + 1 by NAT_1:44;

then A16: m <= k1 by NAT_1:13;

m < n by A2, A15, XXREAL_0:2;

then A17: m in Segm n by NAT_1:44;

then A18: m in dom f by FUNCT_2:def 1;

m <= k1 by A15, NAT_1:13;

then min (m,k1) = m by XXREAL_0:def 9;

then f . m = m by A8, A17;

then A19: f . m in {m} by TARSKI:def 1;

then A20: m in f " {m} by A18, FUNCT_1:def 7;

A21: not f " {m} is empty by A19, A18, FUNCT_1:def 7;

now :: thesis: min* (f " {m}) = mend;

hence
min* (f " {m}) = m
; :: thesis: verumper cases
( m < k1 or m = k1 )
by A16, XXREAL_0:1;

end;

suppose A22:
m < k1
; :: thesis: min* (f " {m}) = m

min* (f " {m}) in f " {m} by A21, NAT_1:def 1;

hence min* (f " {m}) = m by A26, TARSKI:def 1; :: thesis: verum

end;

now :: thesis: for l9 being object st l9 in f " {m} holds

l9 in {m}

then A26:
f " {m} c= {m}
;l9 in {m}

A23:
n is Subset of NAT
by Th8;

let l9 be object ; :: thesis: ( l9 in f " {m} implies l9 in {m} )

assume A24: l9 in f " {m} ; :: thesis: l9 in {m}

l9 in dom f by A24, FUNCT_1:def 7;

then l9 in n ;

then reconsider l = l9 as Element of NAT by A23;

f . l in {m} by A24, FUNCT_1:def 7;

then A25: f . l = m by TARSKI:def 1;

l in dom f by A24, FUNCT_1:def 7;

then min (l,k1) = m by A8, A25;

then l = m by A22, XXREAL_0:15;

hence l9 in {m} by TARSKI:def 1; :: thesis: verum

end;let l9 be object ; :: thesis: ( l9 in f " {m} implies l9 in {m} )

assume A24: l9 in f " {m} ; :: thesis: l9 in {m}

l9 in dom f by A24, FUNCT_1:def 7;

then l9 in n ;

then reconsider l = l9 as Element of NAT by A23;

f . l in {m} by A24, FUNCT_1:def 7;

then A25: f . l = m by TARSKI:def 1;

l in dom f by A24, FUNCT_1:def 7;

then min (l,k1) = m by A8, A25;

then l = m by A22, XXREAL_0:15;

hence l9 in {m} by TARSKI:def 1; :: thesis: verum

min* (f " {m}) in f " {m} by A21, NAT_1:def 1;

hence min* (f " {m}) = m by A26, TARSKI:def 1; :: thesis: verum

suppose A27:
m = k1
; :: thesis: min* (f " {m}) = m

for l being Nat st l in f " {m} holds

m <= l

end;m <= l

proof

hence
min* (f " {m}) = m
by A20, NAT_1:def 1; :: thesis: verum
let l be Nat; :: thesis: ( l in f " {m} implies m <= l )

assume A28: l in f " {m} ; :: thesis: m <= l

f . l in {m} by A28, FUNCT_1:def 7;

then A29: f . l = m by TARSKI:def 1;

l in dom f by A28, FUNCT_1:def 7;

then f . l = min (l,m) by A8, A27;

hence m <= l by A29, XXREAL_0:def 9; :: thesis: verum

end;assume A28: l in f " {m} ; :: thesis: m <= l

f . l in {m} by A28, FUNCT_1:def 7;

then A29: f . l = m by TARSKI:def 1;

l in dom f by A28, FUNCT_1:def 7;

then f . l = min (l,m) by A8, A27;

hence m <= l by A29, XXREAL_0:def 9; :: thesis: verum

now :: thesis: for l, m being Nat st l in rng f & m in rng f & l < m holds

min* (f " {l}) < min* (f " {m})

then
f is "increasing
;min* (f " {l}) < min* (f " {m})

let l, m be Nat; :: thesis: ( l in rng f & m in rng f & l < m implies min* (f " {l}) < min* (f " {m}) )

assume that

A30: l in rng f and

A31: m in rng f and

A32: l < m ; :: thesis: min* (f " {l}) < min* (f " {m})

min* (f " {l}) = l by A14, A30;

hence min* (f " {l}) < min* (f " {m}) by A14, A31, A32; :: thesis: verum

end;assume that

A30: l in rng f and

A31: m in rng f and

A32: l < m ; :: thesis: min* (f " {l}) < min* (f " {m})

min* (f " {l}) = l by A14, A30;

hence min* (f " {l}) < min* (f " {m}) by A14, A31, A32; :: thesis: verum

hence ex f being Function of (Segm n),(Segm k) st

( f is onto & f is "increasing ) by A13; :: thesis: verum

( f is onto & f is "increasing ) ; :: thesis: verum