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 A1, FUNCT_2:def 3;

then consider x being object such that

A4: x in dom f and

A5: f . x = g . n by A3, FUNCT_1:def 3;

g . n = g . x by A2, A4, A5, FUNCT_1:47;

then A6: g . x in {(g . n)} by TARSKI:def 1;

k c= 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 A3, FUNCT_2:def 1;

then x in g " {(g . n)} by A14, A13, A6, FUNCT_1:def 7;

hence g " {(g . n)} <> {n} by A15, TARSKI:def 1; :: thesis: verum

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 A1, FUNCT_2:def 3;

then consider x being object such that

A4: x in dom f and

A5: f . x = g . n by A3, FUNCT_1:def 3;

g . n = g . x by A2, A4, A5, FUNCT_1:47;

then A6: g . x in {(g . n)} by TARSKI:def 1;

k c= rng g

proof

then
k = rng g
;
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 A1, FUNCT_2:def 3;

then consider y being object such that

A10: y in dom f and

A11: f . y = x by A9, FUNCT_1:def 3;

A12: dom g = n + 1 by A3, FUNCT_2:def 1;

f . y = g . y by A2, A10, FUNCT_1:47;

hence x9 in rng g by A10, A11, A8, A7, A12, FUNCT_1:def 3; :: thesis: verum

end;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 A1, FUNCT_2:def 3;

then consider y being object such that

A10: y in dom f and

A11: f . y = x by A9, FUNCT_1:def 3;

A12: dom g = n + 1 by A3, FUNCT_2:def 1;

f . y = g . y by A2, A10, FUNCT_1:47;

hence x9 in rng g by A10, A11, A8, A7, A12, FUNCT_1:def 3; :: thesis: verum

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 A3, FUNCT_2:def 1;

then x in g " {(g . n)} by A14, A13, A6, FUNCT_1:def 7;

hence g " {(g . n)} <> {n} by A15, TARSKI:def 1; :: thesis: verum