let k, n be Nat; :: thesis: for f being Function of (Segm n),(Segm k)
for g being Function of (Segm (n + 1)),(Segm (k + 1)) st f is onto & f is "increasing & f = g | (Segm n) & g . n = k holds
( g is onto & g is "increasing & g " {(g . n)} = {n} )
let f be Function of (Segm n),(Segm k); :: thesis: for g being Function of (Segm (n + 1)),(Segm (k + 1)) st f is onto & f is "increasing & f = g | (Segm n) & g . n = k holds
( g is onto & g is "increasing & g " {(g . n)} = {n} )
let g be Function of (Segm (n + 1)),(Segm (k + 1)); :: thesis: ( f is onto & f is "increasing & f = g | (Segm n) & g . n = k implies ( g is onto & g is "increasing & g " {(g . n)} = {n} ) )
assume that
A1: ( f is onto & f is "increasing ) and
A2: f = g | (Segm n) and
A3: g . n = k ; :: thesis: ( g is onto & g is "increasing & g " {(g . n)} = {n} )
Segm (k + 1) c= rng g

proof

let x9 be object ; :: according to TARSKI:def 3 :: thesis: ( not x9 in Segm (k + 1) or x9 in rng g )
assume A4: x9 in Segm (k + 1) ; :: thesis: x9 in rng g
reconsider x = x9 as Element of NAT by A4;
x < k + 1 by A4, NAT_1:44;
then A5: x <= k by NAT_1:13;

now :: thesis: x9 in rng g

per cases ( x < k or x = k ) by A5, XXREAL_0:1;

suppose A6: x < k ; :: thesis: x9 in rng g

A7: rng f = k by A1, FUNCT_2:def 3;
x in Segm k by A6, NAT_1:44;
then consider y being object such that
A8: y in dom f and
A9: f . y = x by A7, FUNCT_1:def 3;
A10: dom g = n + 1 by FUNCT_2:def 1;
( n = 0 iff k = 0 ) by A1;
then A11: dom f = n by FUNCT_2:def 1;
n <= n + 1 by NAT_1:11;
then A12: Segm n c= Segm (n + 1) by NAT_1:39;
f . y = g . y by A2, A8, FUNCT_1:47;
hence x9 in rng g by A8, A9, A11, A12, A10, FUNCT_1:def 3; :: thesis: verum

end;

suppose A13: x = k ; :: thesis: x9 in rng g

n < n + 1 by NAT_1:13;
then A14: n in Segm (n + 1) by NAT_1:44;
dom g = n + 1 by FUNCT_2:def 1;
hence x9 in rng g by A3, A13, A14, FUNCT_1:def 3; :: thesis: verum

end;

end;

end;

hence x9 in rng g ; :: thesis: verum

end;

then k + 1 = rng g ;
hence g is onto by FUNCT_2:def 3; :: thesis: ( g is "increasing & g " {(g . n)} = {n} )
for i, j being Nat st i in rng g & j in rng g & i < j holds
min* (g " {i}) < min* (g " {j}) by A1, A2, Th39;
hence g is "increasing ; :: thesis: g " {(g . n)} = {n}
thus g " {(g . n)} = {n} :: thesis: verum

proof

assume g " {(g . n)} <> {n} ; :: thesis: contradiction
then consider m being Nat such that
A15: m in g " {(g . n)} and
A16: m <> n by Th35;
g . m in {(g . n)} by A15, FUNCT_1:def 7;
then A17: g . m = k by A3, TARSKI:def 1;
m in dom g by A15, FUNCT_1:def 7;
then m < n + 1 by NAT_1:44;
then m <= n by NAT_1:13;
then A18: m < n by A16, XXREAL_0:1;
( n = 0 iff k = 0 ) by A1;
then dom f = n by FUNCT_2:def 1;
then A19: m in dom f by A18, NAT_1:44;
then A20: f . m in rng f by FUNCT_1:def 3;
f . m = g . m by A2, A19, FUNCT_1:47;
hence contradiction by A20, A17, NAT_1:44; :: thesis: verum

end;