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

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 ) ) )
per cases ( n = 0 or n > 0 ) ;
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 ) ) )

then 0 + 1 >= k + 1 by ;
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 ; :: thesis: verum
end;
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 ) ) )

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 )
proof
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 ;
i in (dom f) /\ n by ;
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 < 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 ;
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 ;
then i in dom f by XBOOLE_0:def 4;
then i in f " {(f . n)} by ;
then ( i >= min* (f " {(f . n)}) & i in NAT & n in NAT ) by ;
then A17: i >= n by ;
i in Segm n by ;
hence contradiction by A17, NAT_1:44; :: thesis: verum
end;
f . i = (f | n) . i by ;
hence fi in Segm k by ; :: thesis: verum
end;
thus for g being Function of (Segm n),(Segm k) st g = f | n holds
( 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
proof
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 ;
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 ;
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 ;
then consider n1 being object such that
A24: n1 in dom f and
A25: f . n1 = k9 by ;
reconsider n1 = n1 as Element of NAT by ;
n1 < n + 1 by ;
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 ;
(dom f) /\ n = dom (f | n) by RELAT_1:61;
then A28: n1 in dom g by ;
then g . n1 in rng g by FUNCT_1:def 3;
hence k1 in rng g by ; :: thesis: verum
end;
then k = 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 ;
0 in Segm n by ;
then (f | n) . 0 in rng (f | n) by ;
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 ;
hence g is "increasing by A32; :: thesis: verum
end;
end;
end;
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 ) ) ) ; :: thesis: verum