let k, n be Nat; :: thesis: for f being Function of (Segm (n + 1)),(Segm (k + 1)) st f is onto & f is "increasing & f " {(f . n)} = {n} holds
f . n = k
let f be Function of (Segm (n + 1)),(Segm (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 :: thesis: contradiction

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:44;
hence contradiction by A4, NAT_1:13; :: thesis: verum

end;

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

A6: min* (f " {k}) <= (n + 1) - 1 by Th16;
A7: rng f = k + 1 by A1, FUNCT_2:def 3;
k < k + 1 by NAT_1:13;
then k in rng f by A7, NAT_1:44;
then ( min* (f " {(f . n)}) < min* (f " {k}) & k in NAT & n in NAT ) by A1, A5, A7, ORDINAL1:def 12;
hence contradiction by A2, A6, Th5; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum