let k, n be Nat; :: thesis: for f being Function of (Segm n),(Segm k) st f is onto & f is "increasing & n = k holds
f = id n
let f be Function of (Segm n),(Segm k); :: thesis: ( f is onto & f is "increasing & n = k implies f = id n )
assume that
A1: ( f is onto & f is "increasing ) and
A2: n = k ; :: thesis: f = id n

now :: thesis: f = id n

per cases ( n = 0 or n > 0 ) ;

suppose A3: n = 0 ; :: thesis: f = id n

thus f = id n by A3; :: thesis: verum

end;

suppose A4: n > 0 ; :: thesis: f = id n

A5: now :: thesis: for m9 being object st m9 in Segm n holds
f . m9 = m9

let m9 be object ; :: thesis: ( m9 in Segm n implies f . m9 = m9 )
assume A6: m9 in Segm n ; :: thesis: f . m9 = m9
reconsider m = m9 as Element of NAT by A6;
m in rng f by A1, A2, A6, FUNCT_2:def 3;
then A7: ex x being object st
( x in dom f & f . x = m ) by FUNCT_1:def 3;
m in {m} by TARSKI:def 1;
then reconsider F = f " {m} as non empty Subset of NAT by A7, FUNCT_1:def 7;
A8: m < k by A2, A6, NAT_1:44;
then A9: m <= min* (f " {m}) by A1, Th18;
(n - k) + m = m by A2;
then min* (f " {m}) <= m by A1, A8, Th19;
then A10: min* F = m by A9, XXREAL_0:1;
min* F in F by NAT_1:def 1;
then f . m in {m} by A10, FUNCT_1:def 7;
hence f . m9 = m9 by TARSKI:def 1; :: thesis: verum

end;

dom f = n by A2, A4, FUNCT_2:def 1;
hence f = id n by A5, FUNCT_1:17; :: thesis: verum

end;

end;

end;

hence f = id n ; :: thesis: verum