let n, k be Element of NAT ; :: thesis: not ( ( n = 0 implies k = 0 ) & ( k = 0 implies n = 0 ) & ( for f being Function of n,k holds not f is "increasing ) )
assume A1: ( n = 0 iff k = 0 ) ; :: thesis: ex f being Function of n,k st 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 "increasing

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

end;

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

then consider f being Function such that
A4: ( dom f = n & rng f = {0 } ) by FUNCT_1:15;
reconsider f = f as Function of n,{0 } by A4, FUNCT_2:3;
A5: for l, m being Element of NAT st l in rng f & m in rng f & l < m holds
min* (f " {l}) < min* (f " {m}) by TARSKI:def 1;
rng f c= k

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng f or x in k )
assume A6: x in rng f ; :: thesis: x in k
( x in {0 } & 0 < k ) by A1, A3, A6;
then ( x = 0 & 0 in k ) by NAT_1:45, TARSKI:def 1;
hence x in k ; :: thesis: verum

end;

then reconsider f = f as Function of n,k by FUNCT_2:8;
f is "increasing by A1, A5, Def1;
hence ex f being Function of n,k st f is "increasing ; :: thesis: verum

end;

end;

end;

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