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 ;
then A5: x <= k by NAT_1:13;
now :: thesis: x9 in rng g
per cases ( x < k or x = k ) by ;
suppose A6: x < k ; :: thesis: x9 in rng g
A7: rng f = k by ;
x in Segm k by ;
then consider y being object such that
A8: y in dom f and
A9: f . y = x by ;
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 ;
hence x9 in rng g by ; :: 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 ;
then A17: g . m = k by ;
m in dom g by ;
then m < n + 1 by NAT_1:44;
then m <= n by NAT_1:13;
then A18: m < n by ;
( n = 0 iff k = 0 ) by A1;
then dom f = n by FUNCT_2:def 1;
then A19: m in dom f by ;
then A20: f . m in rng f by FUNCT_1:def 3;
f . m = g . m by ;
hence contradiction by A20, A17, NAT_1:44; :: thesis: verum
end;