let n, k be Element of NAT ; :: thesis: not ( ( n = 0 implies k = 0 ) & ( k = 0 implies n = 0 ) & n >= k & ( for f being Function of n,k holds
( not f is onto or not f is "increasing ) ) )
assume A1: ( ( n = 0 implies k = 0 ) & ( k = 0 implies n = 0 ) & n >= k ) ; :: thesis: ex f being Function of n,k st
( f is onto & f is "increasing )

now

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

suppose A2: n = 0 ; :: thesis: ex f being Function of n,k st
( f is onto & f is "increasing )

set f = {} ;
( rng {} = k & dom {} = n ) by A1, A2;
then reconsider f = {} as Function of n,k by FUNCT_2:3;
( f is onto & f is "increasing ) by A1, Th15;
hence ex f being Function of n,k st
( f is onto & f is "increasing ) ; :: thesis: verum

end;

suppose A3: n > 0 ; :: thesis: ex f being Function of n,k st
( 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 empty Element of NAT by A1, A3;
defpred S₁[ Element of n, Element of k] means $2 = min $1,k1;
A4: for x being Element of n ex y being Element of k st S₁[x,y]

proof

let x be Element of n; :: thesis: ex y being Element of k st S₁[x,y]
( min x,k1 <= k1 & k1 < k1 + 1 ) by NAT_1:13, XXREAL_0:17;
then ( min x,k1 < k & min x,k1 is natural ) by XXREAL_0:2;
then min x,k1 in k by NAT_1:45;
hence ex y being Element of k st S₁[x,y] ; :: thesis: verum

end;

consider f being Function of n,k such that
A5: for m being Element of n holds S₁[m,f . m] from FUNCT_2:sch 3(A4);
A6: f is onto

proof

now

let m' be set ; :: thesis: ( m' in k implies m' in rng f )
assume A7: m' in k ; :: thesis: m' in rng f
k is Subset of NAT by Th8;
then reconsider m = m' as Element of NAT by A7;
m < k1 + 1 by A7, NAT_1:45;
then ( m < n & m <= k1 ) by A1, NAT_1:13, XXREAL_0:2;
then ( m in n & min m,k1 = m ) by NAT_1:45, XXREAL_0:def 9;
then ( f . m = m & m in dom f ) by A5, FUNCT_2:def 1;
hence m' in rng f by FUNCT_1:def 5; :: thesis: verum

end;

then ( k c= rng f & rng f c= k ) by TARSKI:def 3;
then k = rng f by XBOOLE_0:def 10;
hence f is onto by FUNCT_2:def 3; :: thesis: verum

end;

A8: for m being Element of NAT st m in rng f holds
min* (f " {m}) = m

proof

let m be Element of NAT ; :: thesis: ( m in rng f implies min* (f " {m}) = m )
assume A9: m in rng f ; :: thesis: min* (f " {m}) = m
A10: m < k1 + 1 by A9, NAT_1:45;
then ( m < n & m <= k1 ) by A1, NAT_1:13, XXREAL_0:2;
then ( m in n & min m,k1 = m ) by NAT_1:45, XXREAL_0:def 9;
then ( f . m = m & m in dom f ) by A5, FUNCT_2:def 1;
then ( f . m in {m} & m in dom f ) by TARSKI:def 1;
then A11: ( not f " {m} is empty & m in f " {m} ) by FUNCT_1:def 13;
A12: m <= k1 by A10, NAT_1:13;

now

per cases ( m < k1 or m = k1 ) by A12, XXREAL_0:1;

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

now

let l' be set ; :: thesis: ( l' in f " {m} implies l' in {m} )
assume A14: l' in f " {m} ; :: thesis: l' in {m}
l' in dom f by A14, FUNCT_1:def 13;
then ( l' in n & n is Subset of NAT ) by Th8;
then reconsider l = l' as Element of NAT ;
( l in dom f & f . l in {m} ) by A14, FUNCT_1:def 13;
then ( l in n & f . l = m ) by TARSKI:def 1;
then min l,k1 = m by A5;
then l = m by A13, XXREAL_0:15;
hence l' in {m} by TARSKI:def 1; :: thesis: verum

end;

then ( f " {m} c= {m} & min* (f " {m}) in f " {m} ) by A11, NAT_1:def 1, TARSKI:def 3;
hence min* (f " {m}) = m by TARSKI:def 1; :: thesis: verum

end;

suppose A15: 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 A16: l in f " {m} ; :: thesis: m <= l
( l in dom f & dom f = n & f . l in {m} ) by A16, FUNCT_1:def 13, FUNCT_2:def 1;
then ( f . l = min l,m & f . l = m ) by A5, A15, TARSKI:def 1;
hence m <= l by XXREAL_0:def 9; :: thesis: verum

end;

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

end;

end;

end;

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

end;

now

let l, m be Element of NAT ; :: thesis: ( l in rng f & m in rng f & l < m implies min* (f " {l}) < min* (f " {m}) )
assume A17: ( l in rng f & m in rng f & l < m ) ; :: thesis: min* (f " {l}) < min* (f " {m})
( min* (f " {l}) = l & min* (f " {m}) = m ) by A8, A17;
hence min* (f " {l}) < min* (f " {m}) by A17; :: thesis: verum

end;

then f is "increasing by Def1;
hence ex f being Function of n,k st
( f is onto & f is "increasing ) by A6; :: thesis: verum

end;

end;

end;

hence ex f being Function of n,k st
( f is onto & f is "increasing ) ; :: thesis: verum