let k, m, n be Nat; :: thesis:
let f be Function of (Segm n),(Segm k); :: thesis:
let g be Function of (Segm (n + 1)),(Segm (k + m)); :: thesis:
assume that
A1: ( f is onto & f is "increasing ) and
A2: f = g | n ; :: thesis:
A3: for i being Nat st i < n holds
f . i = g . i

proof

( k = 0 iff n = 0 ) by A1;
then A4: dom f = n by FUNCT_2:def 1;
let i be Nat; :: thesis:
assume i < n ; :: thesis:
then i in Segm n by NAT_1:44;
hence f . i = g . i by A2, A4, FUNCT_1:47; :: thesis:

end;

A5: for l being Nat st l in rng g & not l in rng f holds
l = g . n

proof

let l be Nat; :: thesis:
assume that
A6: l in rng g and
A7: not l in rng f ; :: thesis:
consider x being object such that
A8: x in dom g and
A9: g . x = l by A6, FUNCT_1:def 3;
assume A10: l <> g . n ; :: thesis:
dom g = n + 1 by A6, FUNCT_2:def 1;
then reconsider x = x as Element of NAT by A8;
x < n + 1 by A8, NAT_1:44;
then x <= n by NAT_1:13;
then A11: x < n by A10, A9, XXREAL_0:1;
then A12: x in Segm n by NAT_1:44;
k <> 0 by A1, A11;
then A13: dom f = n by FUNCT_2:def 1;
f . x = g . x by A3, A11;
hence contradiction by A7, A9, A13, A12, FUNCT_1:def 3; :: thesis:

end;

A14: for l being Nat st l in rng g & not l in rng f holds
min* (g " {l}) = n

proof

A15: n < n + 1 by NAT_1:13;
let l be Nat; :: thesis:
assume that
A16: l in rng g and
A17: not l in rng f ; :: thesis:
A18: l in {l} by TARSKI:def 1;
dom g = n + 1 by A16, FUNCT_2:def 1;
then A19: n in dom g by A15, NAT_1:44;
g . n = l by A5, A16, A17;
then n in g " {l} by A19, A18, FUNCT_1:def 7;
then min* (g " {l}) in g " {l} by NAT_1:def 1;
then A20: g . (min* (g " {l})) in {l} by FUNCT_1:def 7;
assume A21: min* (g " {l}) <> n ; :: thesis:
min* (g " {l}) <= (n + 1) - 1 by Th16;
then A22: min* (g " {l}) < n by A21, XXREAL_0:1;
then k <> 0 by A1;
then A23: dom f = n by FUNCT_2:def 1;
min* (g " {l}) in Segm n by A22, NAT_1:44;
then A24: f . (min* (g " {l})) in rng f by A23, FUNCT_1:def 3;
f . (min* (g " {l})) = g . (min* (g " {l})) by A3, A22;
hence contradiction by A17, A20, A24, TARSKI:def 1; :: thesis:

end;

A25: for k1 being Element of NAT st k1 in rng f holds
min* (g " {k1}) = min* (f " {k1})

proof

n <= n + 1 by NAT_1:11;
then A26: Segm n c= Segm (n + 1) by NAT_1:39;
let k1 be Element of NAT ; :: thesis:
assume A27: k1 in rng f ; :: thesis:
consider x being object such that
A28: x in dom f and
A29: f . x = k1 by A27, FUNCT_1:def 3;
A30: x in n by A28;
not Segm k is empty by A27;
then not k is zero ;
then not k + m is zero ;
then not Segm (k + m) is empty ;
then A31: dom g = Segm (n + 1) by FUNCT_2:def 1;
n is Subset of NAT by Th8;
then reconsider x = x as Element of NAT by A30;
k1 in {k1} by TARSKI:def 1;
then A32: x in f " {k1} by A28, A29, FUNCT_1:def 7;
then A33: min* (f " {k1}) <= x by NAT_1:def 1;
A34: x < n by A28, NAT_1:44;
then A35: min* (f " {k1}) < n by A33, XXREAL_0:2;
A36: dom f = n by A27, FUNCT_2:def 1;

A37: now :: thesis:

let n1 be Nat; :: thesis:
assume A38: n1 in g " {k1} ; :: thesis:
n1 in Segm (n + 1) by A31, A38, FUNCT_1:def 7;
then n1 < n + 1 by NAT_1:44;
then A39: n1 <= n by NAT_1:13;

now :: thesis:

per cases by A39, XXREAL_0:1;

suppose A40: n1 < n ; :: thesis:

g . n1 in {k1} by A38, FUNCT_1:def 7;
then A41: f . n1 in {k1} by A3, A40;
n1 in dom f by A36, A40, NAT_1:44;
then n1 in f " {k1} by A41, FUNCT_1:def 7;
hence min* (f " {k1}) <= n1 by NAT_1:def 1; :: thesis:

end;

suppose n1 = n ; :: thesis:

hence min* (f " {k1}) <= n1 by A33, A34, XXREAL_0:2; :: thesis:

end;

end;

end;

hence min* (f " {k1}) <= n1 ; :: thesis:

end;

min* (f " {k1}) in f " {k1} by A32, NAT_1:def 1;
then f . (min* (f " {k1})) in {k1} by FUNCT_1:def 7;
then A42: g . (min* (f " {k1})) in {k1} by A3, A35;
min* (f " {k1}) in n by A35, NAT_1:44;
then min* (f " {k1}) in g " {k1} by A31, A26, A42, FUNCT_1:def 7;
hence min* (g " {k1}) = min* (f " {k1}) by A37, NAT_1:def 1; :: thesis:

end;

let i, j be Nat; :: thesis:
assume that
A43: i in rng g and
A44: j in rng g and
A45: i < j ; :: thesis:
A46: for l being Nat st l in rng g & not l in rng f holds
l >= k

proof

let l be Nat; :: thesis:
assume that
l in rng g and
A47: not l in rng f ; :: thesis:
assume l < k ; :: thesis:
then l in Segm k by NAT_1:44;
hence contradiction by A1, A47, FUNCT_2:def 3; :: thesis:

end;

A48: ( i in NAT & j in NAT ) by ORDINAL1:def 12;

now :: thesis:

per cases ;

suppose A49: ( i in rng f & j in rng f ) ; :: thesis:

then A50: min* (g " {j}) = min* (f " {j}) by A25, A48;
min* (g " {i}) = min* (f " {i}) by A25, A49, A48;
hence min* (g " {i}) < min* (g " {j}) by A1, A45, A49, A50; :: thesis:

end;

suppose A51: ( i in rng f & not j in rng f ) ; :: thesis:

then A52: n <> 0 ;
then min* (f " {i}) <= n - 1 by Th16;
then A53: min* (g " {i}) <= n - 1 by A25, A51, A48;
n - 1 is Element of NAT by A52, NAT_1:20;
then A54: n - 1 < (n - 1) + 1 by NAT_1:13;
min* (g " {j}) = n by A44, A14, A51;
hence min* (g " {i}) < min* (g " {j}) by A53, A54, XXREAL_0:2; :: thesis:

end;

suppose A55: ( not i in rng f & j in rng f ) ; :: thesis:

then A56: j < k by NAT_1:44;
i >= k by A43, A46, A55;
hence min* (g " {i}) < min* (g " {j}) by A45, A56, XXREAL_0:2; :: thesis:

end;

suppose A57: ( not i in rng f & not j in rng f ) ; :: thesis:

then i = g . n by A43, A5;
hence min* (g " {i}) < min* (g " {j}) by A44, A45, A5, A57; :: thesis:

end;

end;

end;

hence min* (g " {i}) < min* (g " {j}) ; :: thesis: