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 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 ;
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 ;
A8: m < k by ;
then A9: m <= min* (f " {m}) by ;
(n - k) + m = m by A2;
then min* (f " {m}) <= m by A1, A8, Th19;
then A10: min* F = m by ;
min* F in F by NAT_1:def 1;
then f . m in {m} by ;
hence f . m9 = m9 by TARSKI:def 1; :: thesis: verum
end;
dom f = n by ;
hence f = id n by ; :: thesis: verum
end;
end;
end;
hence f = id n ; :: thesis: verum