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 ;
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 = by FUNCT_1:5;
reconsider f = f as Function of n, by ;
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 ;
hence x in Segm k by ; :: 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 ;
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