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

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

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

then
k + 1 = rng g
;
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;

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

hence
x9 in rng g
; :: thesis: verumper cases
( x < k or x = k )
by A5, XXREAL_0:1;

end;

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

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