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) 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) 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); :: 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} )
k = rng f by ;
then consider x being object such that
A4: x in dom f and
A5: f . x = g . n by ;
g . n = g . x by ;
then A6: g . x in {(g . n)} by TARSKI:def 1;
k c= rng g
proof
n <= n + 1 by NAT_1:13;
then A7: Segm n c= Segm (n + 1) by NAT_1:39;
( n = 0 iff k = 0 ) by A1;
then A8: dom f = n by FUNCT_2:def 1;
let x9 be object ; :: according to TARSKI:def 3 :: thesis: ( not x9 in k or x9 in rng g )
assume A9: x9 in k ; :: thesis: x9 in rng g
k is Subset of NAT by Th8;
then reconsider x = x9 as Element of NAT by A9;
rng f = k by ;
then consider y being object such that
A10: y in dom f and
A11: f . y = x by ;
A12: dom g = n + 1 by ;
f . y = g . y by ;
hence x9 in rng g by ; :: thesis: verum
end;
then k = rng g ;
hence g is onto by FUNCT_2:def 3; :: thesis: ( g is "increasing & g " {(g . n)} <> {n} )
k = k + 0 ;
then 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 by A3; :: thesis: g " {(g . n)} <> {n}
n <= n + 1 by NAT_1:11;
then A13: Segm n c= Segm (n + 1) by NAT_1:39;
reconsider nn = n as set ;
A: not nn in nn ;
A14: x in n by A4;
then A15: x <> n by A;
dom g = n + 1 by ;
then x in g " {(g . n)} by ;
hence g " {(g . n)} <> {n} by ; :: thesis: verum