let k, n be Nat; :: thesis: for f being Function of (Segm (n + 1)),(Segm (k + 1)) st f is onto & f is "increasing & f " {(f . n)} = {n} holds

( rng (f | n) c= Segm k & ( for g being Function of (Segm n),(Segm k) st g = f | n holds

( g is onto & g is "increasing ) ) )

let f be Function of (Segm (n + 1)),(Segm (k + 1)); :: thesis: ( f is onto & f is "increasing & f " {(f . n)} = {n} implies ( rng (f | n) c= Segm k & ( for g being Function of (Segm n),(Segm k) st g = f | n holds

( g is onto & g is "increasing ) ) ) )

assume that

A1: ( f is onto & f is "increasing ) and

A2: f " {(f . n)} = {n} ; :: thesis: ( rng (f | n) c= Segm k & ( for g being Function of (Segm n),(Segm k) st g = f | n holds

( g is onto & g is "increasing ) ) )

( g is onto & g is "increasing ) ) ) ; :: thesis: verum

( rng (f | n) c= Segm k & ( for g being Function of (Segm n),(Segm k) st g = f | n holds

( g is onto & g is "increasing ) ) )

let f be Function of (Segm (n + 1)),(Segm (k + 1)); :: thesis: ( f is onto & f is "increasing & f " {(f . n)} = {n} implies ( rng (f | n) c= Segm k & ( for g being Function of (Segm n),(Segm k) st g = f | n holds

( g is onto & g is "increasing ) ) ) )

assume that

A1: ( f is onto & f is "increasing ) and

A2: f " {(f . n)} = {n} ; :: thesis: ( rng (f | n) c= Segm k & ( for g being Function of (Segm n),(Segm k) st g = f | n holds

( g is onto & g is "increasing ) ) )

now :: thesis: ( rng (f | n) c= Segm k & ( for g being Function of (Segm n),(Segm k) st g = f | n holds

( g is onto & g is "increasing ) ) )end;

hence
( rng (f | n) c= Segm k & ( for g being Function of (Segm n),(Segm k) st g = f | n holds ( g is onto & g is "increasing ) ) )

per cases
( n = 0 or n > 0 )
;

end;

suppose A3:
n = 0
; :: thesis: ( rng (f | n) c= Segm k & ( for g being Function of (Segm n),(Segm k) st g = f | n holds

( g is onto & g is "increasing ) ) )

( g is onto & g is "increasing ) ) )

then
0 + 1 >= k + 1
by A1, Th17;

then k = 0 by XREAL_1:6;

hence ( rng (f | n) c= Segm k & ( for g being Function of (Segm n),(Segm k) st g = f | n holds

( g is onto & g is "increasing ) ) ) by A3, Th15; :: thesis: verum

end;then k = 0 by XREAL_1:6;

hence ( rng (f | n) c= Segm k & ( for g being Function of (Segm n),(Segm k) st g = f | n holds

( g is onto & g is "increasing ) ) ) by A3, Th15; :: thesis: verum

suppose A4:
n > 0
; :: thesis: ( rng (f | n) c= Segm k & ( for g being Function of (Segm n),(Segm k) st g = f | n holds

( g is onto & g is "increasing ) ) )

( g is onto & g is "increasing ) ) )

thus A5:
rng (f | n) c= Segm k
:: thesis: for g being Function of (Segm n),(Segm k) st g = f | n holds

( g is onto & g is "increasing )

( g is onto & g is "increasing ) :: thesis: verum

end;( g is onto & g is "increasing )

proof

thus
for g being Function of (Segm n),(Segm k) st g = f | n holds
let fi be object ; :: according to TARSKI:def 3 :: thesis: ( not fi in rng (f | n) or fi in Segm k )

assume A6: fi in rng (f | n) ; :: thesis: fi in Segm k

rng (f | n) c= rng f by RELAT_1:70;

then fi in rng f by A6;

then A7: fi in k + 1 ;

k + 1 is Subset of NAT by Th8;

then reconsider fi = fi as Element of NAT by A7;

consider i being object such that

A8: i in dom (f | n) and

A9: (f | n) . i = fi by A6, FUNCT_1:def 3;

i in (dom f) /\ n by A8, RELAT_1:61;

then A10: i in n by XBOOLE_0:def 4;

n is Subset of NAT by Th8;

then reconsider i = i as Element of NAT by A10;

A11: f . i < k

hence fi in Segm k by A9, A11, NAT_1:44; :: thesis: verum

end;assume A6: fi in rng (f | n) ; :: thesis: fi in Segm k

rng (f | n) c= rng f by RELAT_1:70;

then fi in rng f by A6;

then A7: fi in k + 1 ;

k + 1 is Subset of NAT by Th8;

then reconsider fi = fi as Element of NAT by A7;

consider i being object such that

A8: i in dom (f | n) and

A9: (f | n) . i = fi by A6, FUNCT_1:def 3;

i in (dom f) /\ n by A8, RELAT_1:61;

then A10: i in n by XBOOLE_0:def 4;

n is Subset of NAT by Th8;

then reconsider i = i as Element of NAT by A10;

A11: f . i < k

proof

f . i = (f | n) . i
by A8, FUNCT_1:47;
f . i < k + 1
by NAT_1:44;

then A12: f . i <= k by NAT_1:13;

assume f . i >= k ; :: thesis: contradiction

then A13: f . i = k by A12, XXREAL_0:1;

A14: f . i in {(f . i)} by TARSKI:def 1;

A15: f . n = k by A1, A2, Th34;

A16: i in (dom f) /\ n by A8, RELAT_1:61;

then i in dom f by XBOOLE_0:def 4;

then i in f " {(f . n)} by A13, A14, A15, FUNCT_1:def 7;

then ( i >= min* (f " {(f . n)}) & i in NAT & n in NAT ) by NAT_1:def 1, ORDINAL1:def 12;

then A17: i >= n by A2, Th5;

i in Segm n by A16, XBOOLE_0:def 4;

hence contradiction by A17, NAT_1:44; :: thesis: verum

end;then A12: f . i <= k by NAT_1:13;

assume f . i >= k ; :: thesis: contradiction

then A13: f . i = k by A12, XXREAL_0:1;

A14: f . i in {(f . i)} by TARSKI:def 1;

A15: f . n = k by A1, A2, Th34;

A16: i in (dom f) /\ n by A8, RELAT_1:61;

then i in dom f by XBOOLE_0:def 4;

then i in f " {(f . n)} by A13, A14, A15, FUNCT_1:def 7;

then ( i >= min* (f " {(f . n)}) & i in NAT & n in NAT ) by NAT_1:def 1, ORDINAL1:def 12;

then A17: i >= n by A2, Th5;

i in Segm n by A16, XBOOLE_0:def 4;

hence contradiction by A17, NAT_1:44; :: thesis: verum

hence fi in Segm k by A9, A11, NAT_1:44; :: thesis: verum

( g is onto & g is "increasing ) :: thesis: verum

proof

let g be Function of (Segm n),(Segm k); :: thesis: ( g = f | n implies ( g is onto & g is "increasing ) )

assume A18: g = f | n ; :: thesis: ( g is onto & g is "increasing )

Segm k c= rng g

hence g is onto by FUNCT_2:def 3; :: thesis: g is "increasing

A29: (dom f) /\ n = dom (f | n) by RELAT_1:61;

n < n + 1 by NAT_1:13;

then A30: Segm n c= Segm (n + 1) by NAT_1:39;

dom f = n + 1 by FUNCT_2:def 1;

then A31: n = (dom f) /\ n by A30, XBOOLE_1:28;

0 in Segm n by A4, NAT_1:44;

then (f | n) . 0 in rng (f | n) by A31, A29, FUNCT_1:def 3;

then A32: ( n = 0 iff k = 0 ) by A5;

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, A18, Th36;

hence g is "increasing by A32; :: thesis: verum

end;assume A18: g = f | n ; :: thesis: ( g is onto & g is "increasing )

Segm k c= rng g

proof

then
k = rng g
;
n < n + 1
by NAT_1:13;

then A19: Segm n c= Segm (n + 1) by NAT_1:39;

dom f = n + 1 by FUNCT_2:def 1;

then A20: n = (dom f) /\ n by A19, XBOOLE_1:28;

let k1 be object ; :: according to TARSKI:def 3 :: thesis: ( not k1 in Segm k or k1 in rng g )

assume A21: k1 in Segm k ; :: thesis: k1 in rng g

reconsider k9 = k1 as Element of NAT by A21;

k9 < k by A21, NAT_1:44;

then k9 < k + 1 by NAT_1:13;

then A22: k9 in Segm (k + 1) by NAT_1:44;

A23: dom f = n + 1 by FUNCT_2:def 1;

rng f = k + 1 by A1, FUNCT_2:def 3;

then consider n1 being object such that

A24: n1 in dom f and

A25: f . n1 = k9 by A22, FUNCT_1:def 3;

reconsider n1 = n1 as Element of NAT by A24, A23;

n1 < n + 1 by A24, NAT_1:44;

then A26: n1 <= n by NAT_1:13;

reconsider nn = k1 as set by TARSKI:1;

A: not nn in nn ;

f . n = k by A1, A2, Th34;

then n1 <> n by A, A21, A25;

then A27: n1 < n by A26, XXREAL_0:1;

(dom f) /\ n = dom (f | n) by RELAT_1:61;

then A28: n1 in dom g by A18, A27, A20, NAT_1:44;

then g . n1 in rng g by FUNCT_1:def 3;

hence k1 in rng g by A18, A25, A28, FUNCT_1:47; :: thesis: verum

end;then A19: Segm n c= Segm (n + 1) by NAT_1:39;

dom f = n + 1 by FUNCT_2:def 1;

then A20: n = (dom f) /\ n by A19, XBOOLE_1:28;

let k1 be object ; :: according to TARSKI:def 3 :: thesis: ( not k1 in Segm k or k1 in rng g )

assume A21: k1 in Segm k ; :: thesis: k1 in rng g

reconsider k9 = k1 as Element of NAT by A21;

k9 < k by A21, NAT_1:44;

then k9 < k + 1 by NAT_1:13;

then A22: k9 in Segm (k + 1) by NAT_1:44;

A23: dom f = n + 1 by FUNCT_2:def 1;

rng f = k + 1 by A1, FUNCT_2:def 3;

then consider n1 being object such that

A24: n1 in dom f and

A25: f . n1 = k9 by A22, FUNCT_1:def 3;

reconsider n1 = n1 as Element of NAT by A24, A23;

n1 < n + 1 by A24, NAT_1:44;

then A26: n1 <= n by NAT_1:13;

reconsider nn = k1 as set by TARSKI:1;

A: not nn in nn ;

f . n = k by A1, A2, Th34;

then n1 <> n by A, A21, A25;

then A27: n1 < n by A26, XXREAL_0:1;

(dom f) /\ n = dom (f | n) by RELAT_1:61;

then A28: n1 in dom g by A18, A27, A20, NAT_1:44;

then g . n1 in rng g by FUNCT_1:def 3;

hence k1 in rng g by A18, A25, A28, FUNCT_1:47; :: thesis: verum

hence g is onto by FUNCT_2:def 3; :: thesis: g is "increasing

A29: (dom f) /\ n = dom (f | n) by RELAT_1:61;

n < n + 1 by NAT_1:13;

then A30: Segm n c= Segm (n + 1) by NAT_1:39;

dom f = n + 1 by FUNCT_2:def 1;

then A31: n = (dom f) /\ n by A30, XBOOLE_1:28;

0 in Segm n by A4, NAT_1:44;

then (f | n) . 0 in rng (f | n) by A31, A29, FUNCT_1:def 3;

then A32: ( n = 0 iff k = 0 ) by A5;

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, A18, Th36;

hence g is "increasing by A32; :: thesis: verum

( g is onto & g is "increasing ) ) ) ; :: thesis: verum