let k, n be Element of NAT ; :: thesis: for f being Function of n,k st f = id n & n > 0 holds
f is "increasing
let f be Function of n,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
rng f = n by A1, RELAT_1:71;
then A3: ( n c= k & ex x being set st x in n ) by A2, XBOOLE_0:def 1;

now

let l, m be Element of NAT ; :: thesis: ( l in rng f & m in rng f & l < m implies min* (f " {l}) < min* (f " {m}) )
assume A4: ( l in rng f & m in rng f & l < m ) ; :: thesis: min* (f " {l}) < min* (f " {m})
consider l' being set such that
A5: ( l' in dom f & f . l' = l ) by A4, FUNCT_1:def 5;
consider m' being set such that
A6: ( m' in dom f & f . m' = m ) by A4, FUNCT_1:def 5;
( l = l' & l in {l} & m = m' & m in {m} & f is one-to-one ) by A1, A5, A6, FUNCT_1:35, TARSKI:def 1;
then ( l in f " {l} & m in f " {m} & ex x being set st f " {l} = {x} & ex x being set st f " {m} = {x} ) by A4, A5, A6, FUNCT_1:144, FUNCT_1:def 13;
then ( f " {l} = {l} & f " {m} = {m} ) by TARSKI:def 1;
then ( min* (f " {l}) = l & min* (f " {m}) = m ) by Th5;
hence min* (f " {l}) < min* (f " {m}) by A4; :: thesis: verum

end;

hence f is "increasing by A3, Def1; :: thesis: verum