let n, k be Element of 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

then ( dom f = 0 & ( for x being set st x in 0 holds
f . x = x ) ) ;
hence f = id n by A3, FUNCT_1:34; :: thesis: verum

end;

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

A5: now

let m' be set ; :: thesis: ( m' in n implies f . m' = m' )
assume A6: m' in n ; :: thesis: f . m' = m'
n is Subset of NAT by Th8;
then reconsider m = m' as Element of NAT by A6;
m in rng f by A1, A2, A6, FUNCT_2:def 3;
then ( m in {m} & ex x being set st
( x in dom f & f . x = m ) ) by FUNCT_1:def 5, TARSKI:def 1;
then reconsider F = f " {m} as non empty Subset of NAT by FUNCT_1:def 13;
( 0 <= m & m < k & (n - k) + m = m ) by A2, A6, NAT_1:45;
then ( m <= min* (f " {m}) & min* (f " {m}) <= m ) by A1, Th18, Th19;
then ( min* F = m & min* F in F ) by NAT_1:def 1, XXREAL_0:1;
then f . m in {m} by FUNCT_1:def 13;
hence f . m' = m' 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:34; :: thesis: verum

end;

end;

end;

hence f = id n ; :: thesis: verum