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

proof

k + 1 c= rng g

proof

let x' be set ; :: according to TARSKI:def 3 :: thesis: ( not x' in k + 1 or x' in rng g )
assume A4: x' in k + 1 ; :: thesis: x' in rng g
k + 1 is Subset of NAT by Th8;
then reconsider x = x' as Element of NAT by A4;
x < k + 1 by A4, NAT_1:45;
then A5: x <= k by NAT_1:13;

now

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

suppose x < k ; :: thesis: x' in rng g

then ( x in k & rng f = k ) by A1, FUNCT_2:def 3, NAT_1:45;
then consider y being set such that
A6: ( y in dom f & f . y = x ) by FUNCT_1:def 5;
( ( n = 0 implies k = 0 ) & ( k = 0 implies n = 0 ) & n <= n + 1 ) by A1, Def1, NAT_1:11;
then ( dom f = n & n c= n + 1 & dom g = n + 1 ) by FUNCT_2:def 1, NAT_1:40;
then ( y in dom g & f . y = g . y ) by A2, A6, FUNCT_1:70;
hence x' in rng g by A6, FUNCT_1:def 5; :: thesis: verum

end;

suppose A7: x = k ; :: thesis: x' in rng g

n < n + 1 by NAT_1:13;
then ( n in n + 1 & dom g = n + 1 ) by FUNCT_2:def 1, NAT_1:45;
hence x' in rng g by A3, A7, FUNCT_1:def 5; :: thesis: verum

end;

end;

end;

hence x' in rng g ; :: thesis: verum

end;

then k + 1 = rng g by XBOOLE_0:def 10;
hence g is onto by FUNCT_2:def 3; :: thesis: verum

end;

for i, j being Element of 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 Def1; :: thesis: g " {(g . n)} = {n}
thus g " {(g . n)} = {n} :: thesis: verum

proof

assume g " {(g . n)} <> {n} ; :: thesis: contradiction
then consider m being Element of NAT such that
A8: ( m in g " {(g . n)} & m <> n ) by Th35;
( m in dom g & dom g = n + 1 ) by A8, FUNCT_1:def 13, FUNCT_2:def 1;
then m < n + 1 by NAT_1:45;
then ( m <= n & ( n = 0 implies k = 0 ) & ( k = 0 implies n = 0 ) ) by A1, Def1, NAT_1:13;
then ( m < n & dom f = n ) by A8, FUNCT_2:def 1, XXREAL_0:1;
then ( m in dom f & g . m in {(g . n)} ) by A8, FUNCT_1:def 13, NAT_1:45;
then ( f . m in rng f & f . m = g . m & g . m = k ) by A2, A3, FUNCT_1:70, FUNCT_1:def 5, TARSKI:def 1;
hence contradiction by NAT_1:45; :: thesis: verum

end;