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;

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

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})

rng f = n
by A1;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;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

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