let n, k be Nat; :: thesis: for f being Function of n,k st f is onto & f is "increasing & n = k holds
f = id n
let f be Function of n,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

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

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

A4: for x being set st x in 0 holds
f . x = x ;
dom f = 0 by A3;
hence f = id n by A3, A4, FUNCT_1:17; :: thesis: verum

end;

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

A6: now

let m9 be set ; :: thesis: ( m9 in n implies f . m9 = m9 )
assume A7: m9 in n ; :: thesis: f . m9 = m9
n is Subset of NAT by Th8;
then reconsider m = m9 as Element of NAT by A7;
m in rng f by A1, A2, A7, FUNCT_2:def 3;
then A8: ex x being set 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, FUNCT_1:def 7;
A9: m < k by A2, A7, NAT_1:44;
then A10: m <= min* (f " {m}) by A1, Th18;
(n - k) + m = m by A2;
then min* (f " {m}) <= m by A1, A9, Th19;
then A11: min* F = m by A10, XXREAL_0:1;
min* F in F by NAT_1:def 1;
then f . m in {m} by A11, FUNCT_1:def 7;
hence f . m9 = m9 by TARSKI:def 1; :: thesis: verum

end;

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

end;

end;

end;

hence f = id n ; :: thesis: verum