let k, n be Nat; :: thesis: for f being Function of (Segm n),(Segm k) st f = id n & n > 0 holds
f is "increasing
let f be Function of (Segm n),(Segm k); :: thesis: ( f = id n & n > 0 implies f is "increasing )
assume that
A1: f = id n and
A2: n > 0 ; :: thesis: f is "increasing
A3: ex x being object st x in n by A2, XBOOLE_0:def 1;

A4: 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
A5: l in rng f and
A6: m in rng f and
A7: l < m ; :: thesis: min* (f " {l}) < min* (f " {m})
A8: ex x being object st f " {l} = {x} by A1, A5, FUNCT_1:74;
A9: l in {l} by TARSKI:def 1;
consider l9 being object such that
A10: l9 in dom f and
A11: f . l9 = l by A5, FUNCT_1:def 3;
l = l9 by A1, A10, A11, FUNCT_1:18;
then l in f " {l} by A10, A11, A9, FUNCT_1:def 7;
then ( f " {l} = {l} & l in NAT ) by A8, TARSKI:def 1;
then A12: min* (f " {l}) = l by Th5;
A13: m in {m} by TARSKI:def 1;
A14: ex x being object st f " {m} = {x} by A1, A6, FUNCT_1:74;
consider m9 being object such that
A15: m9 in dom f and
A16: f . m9 = m by A6, FUNCT_1:def 3;
m = m9 by A1, A15, A16, FUNCT_1:18;
then m in f " {m} by A15, A16, A13, FUNCT_1:def 7;
then ( f " {m} = {m} & m in NAT ) by A14, TARSKI:def 1;
hence min* (f " {l}) < min* (f " {m}) by A7, A12, Th5; :: thesis: verum

end;

rng f = n by A1;
hence f is "increasing by A3, A4; :: thesis: verum