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 ;
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 ;
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 ;
l = l9 by ;
then l in f " {l} by ;
then ( f " {l} = {l} & l in NAT ) by ;
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 ;
consider m9 being object such that
A15: m9 in dom f and
A16: f . m9 = m by ;
m = m9 by ;
then m in f " {m} by ;
then ( f " {m} = {m} & m in NAT ) by ;
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