let k, n be Nat; :: thesis: not ( ( n = 0 implies k = 0 ) & ( k = 0 implies n = 0 ) & ( for f being Function of (Segm n),(Segm k) holds not f is "increasing ) )
assume A1: ( n = 0 iff k = 0 ) ; :: thesis: ex f being Function of (Segm n),(Segm k) st f is "increasing

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

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

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

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

end;

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

then consider f being Function such that
A4: dom f = n and
A5: rng f = {0} by FUNCT_1:5;
reconsider f = f as Function of n,{0} by A4, A5, FUNCT_2:1;
rng f c= Segm k

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng f or x in Segm k )
assume A6: x in rng f ; :: thesis: x in Segm k
x = 0 by A6, TARSKI:def 1;
hence x in Segm k by A1, A6, NAT_1:44; :: thesis: verum

end;

then reconsider f = f as Function of (Segm n),(Segm k) by FUNCT_2:6;
for l, m being Nat st l in rng f & m in rng f & l < m holds
min* (f " {l}) < min* (f " {m}) by A5, TARSKI:def 1;
then f is "increasing by A1;
hence ex f being Function of (Segm n),(Segm k) st f is "increasing ; :: thesis: verum

end;

end;

end;

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