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

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: contradictionend;

hence
contradiction
; :: thesis: verumper cases
( f . n > k or f . n < k )
by A3, XXREAL_0:1;

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;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