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

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 A1, NAT_1:20;
reconsider k = k, n = n as non zero Element of NAT by A1, A5, ORDINAL1:def 12;
defpred S₁[ 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₁[x,y]

proof

let x be Element of Segm n; :: thesis: ex y being Element of Segm k st S₁[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₁[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 S₁[m,f . m] from FUNCT_2:sch 3(A6);

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

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 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}) = m

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

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

then A26: f " {m} c= {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;

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

hence min* (f " {m}) = m by A20, NAT_1:def 1; :: 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 A14, A30;
hence min* (f " {l}) < min* (f " {m}) by A14, A31, A32; :: 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