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 )

now :: thesis: ex f being Function of (Segm n),(Segm k) st
( f is onto & f is "increasing )
per cases ( n = 0 or n > 0 ) ;
suppose A3: n = 0 ; :: thesis: ex f being Function of (Segm n),(Segm k) st
( 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 ;
( f is onto & f is "increasing ) by ;
hence ex f being Function of (Segm n),(Segm k) st
( f is onto & f is "increasing ) ; :: thesis: verum
end;
suppose A5: n > 0 ; :: thesis: ex f being Function of (Segm n),(Segm k) st
( f is onto & f is "increasing )

then reconsider k1 = k - 1 as Element of NAT by ;
reconsider k = k, n = n as non zero Element of NAT by ;
defpred S1[ 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 S1[x,y]
proof
let x be Element of Segm n; :: thesis: ex y being Element of Segm k st S1[x,y]
A7: k1 < k1 + 1 by NAT_1:13;
min (x,k1) <= k1 by XXREAL_0:17;
then min (x,k1) < k by ;
then min (x,k1) in Segm k by NAT_1:44;
hence ex y being Element of Segm k st S1[x,y] ; :: thesis: verum
end;
consider f being Function of (Segm n),(Segm k) such that
A8: for m being Element of Segm n holds S1[m,f . m] from
now :: thesis: for m9 being object st m9 in Segm k holds
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 ;
then m < n by ;
then A11: m in Segm n by NAT_1:44;
then A12: m in dom f by FUNCT_2:def 1;
m <= k1 by ;
then min (m,k1) = m by XXREAL_0:def 9;
then f . m = m by ;
hence m9 in rng f by ; :: thesis: verum
end;
then k c= rng f ;
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 ;
then A17: m in Segm n by NAT_1:44;
then A18: m in dom f by FUNCT_2:def 1;
m <= k1 by ;
then min (m,k1) = m by XXREAL_0:def 9;
then f . m = m by ;
then A19: f . m in {m} by TARSKI:def 1;
then A20: m in f " {m} by ;
A21: not f " {m} is empty by ;
now :: thesis: min* (f " {m}) = m
per cases ( m < k1 or m = k1 ) by ;
suppose A22: m < k1 ; :: thesis: min* (f " {m}) = m
now :: thesis: for l9 being object st l9 in f " {m} holds
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 ;
then l9 in n ;
then reconsider l = l9 as Element of NAT by A23;
f . l in {m} by ;
then A25: f . l = m by TARSKI:def 1;
l in dom f by ;
then min (l,k1) = m by ;
then l = m by ;
hence l9 in {m} by TARSKI:def 1; :: thesis: verum
end;
then A26: f " {m} c= {m} ;
min* (f " {m}) in f " {m} by ;
hence min* (f " {m}) = m by ; :: thesis: verum
end;
suppose A27: m = k1 ; :: thesis: min* (f " {m}) = m
for l being Nat st l in f " {m} holds
m <= l
proof
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 ;
then A29: f . l = m by TARSKI:def 1;
l in dom f by ;
then f . l = min (l,m) by ;
hence m <= l by ; :: thesis: verum
end;
hence min* (f " {m}) = m by ; :: thesis: verum
end;
end;
end;
hence min* (f " {m}) = m ; :: thesis: verum
end;
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})
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 ;
hence min* (f " {l}) < min* (f " {m}) by ; :: thesis: verum
end;
then f is "increasing ;
hence ex f being Function of (Segm n),(Segm k) st
( f is onto & f is "increasing ) by A13; :: thesis: verum
end;
end;
end;
hence ex f being Function of (Segm n),(Segm k) st
( f is onto & f is "increasing ) ; :: thesis: verum