let n, k be Element of NAT ; :: thesis: for f being Function of n + 1,k + 1 st f is onto & f is "increasing & f " {(f . n)} = {n} holds
f . n = k
let f be Function of n + 1,k + 1; :: thesis: ( f is onto & f is "increasing & f " {(f . n)} = {n} implies f . n = k )
assume that
A1: ( f is onto & f is "increasing ) and
A2: f " {(f . n)} = {n} ; :: thesis: f . n = k
assume A3: f . n <> k ; :: thesis: contradiction

now

per cases ( f . n > k or f . n < k ) by A3, XXREAL_0:1;

suppose A4: f . n > k ; :: thesis: contradiction

f . n < k + 1 by NAT_1:45;
hence contradiction by A4, NAT_1:13; :: thesis: verum

end;

suppose A5: f . n < k ; :: thesis: contradiction

A6: f . n in k + 1 ;
A7: min* (f " {k}) <= (n + 1) - 1 by Th16;
A8: rng f = k + 1 by A1, FUNCT_2:def 3;
k < k + 1 by NAT_1:13;
then A9: k in rng f by A8, NAT_1:45;
k + 1 is Subset of by Th8;
then min* (f " {(f . n)}) < min* (f " {k}) by A1, A5, A8, A6, A9, Def1;
hence contradiction by A2, A7, Th5; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum