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

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

hence
ex f being Function of (Segm n),(Segm k) st f is "increasing
; :: thesis: verumper cases
( n = 0 or n > 0 )
;

end;

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

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

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

then reconsider f = f as Function of (Segm n),(Segm k) by FUNCT_2:6;
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;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

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