let k, l, m, n be Nat; :: thesis: for f being Function of (Segm n),(Segm k)
for g being Function of (Segm (n + m)),(Segm (k + l)) st g is "increasing & f = g | n holds
for i, j being Nat st i in rng f & j in rng f & i < j holds
min* (f " {i}) < min* (f " {j})
let f be Function of (Segm n),(Segm k); :: thesis: for g being Function of (Segm (n + m)),(Segm (k + l)) st g is "increasing & f = g | n holds
for i, j being Nat st i in rng f & j in rng f & i < j holds
min* (f " {i}) < min* (f " {j})
let g be Function of (Segm (n + m)),(Segm (k + l)); :: thesis: ( g is "increasing & f = g | n implies for i, j being Nat st i in rng f & j in rng f & i < j holds
min* (f " {i}) < min* (f " {j}) )
assume that
A1: g is "increasing and
A2: f = g | n ; :: thesis: for i, j being Nat st i in rng f & j in rng f & i < j holds
min* (f " {i}) < min* (f " {j})
let i, j be Nat; :: thesis: ( i in rng f & j in rng f & i < j implies min* (f " {i}) < min* (f " {j}) )
assume that
A3: i in rng f and
A4: j in rng f and
A5: i < j ; :: thesis: min* (f " {i}) < min* (f " {j})
A6: for k1 being Element of NAT st k1 in rng f holds
( k1 in rng g & min* (f " {k1}) = min* (g " {k1}) )

proof

A7: n is Subset of NAT by Th8;
let k1 be Element of NAT ; :: thesis: ( k1 in rng f implies ( k1 in rng g & min* (f " {k1}) = min* (g " {k1}) ) )
assume A8: k1 in rng f ; :: thesis: ( k1 in rng g & min* (f " {k1}) = min* (g " {k1}) )
consider x being object such that
A9: x in dom f and
A10: f . x = k1 by A8, FUNCT_1:def 3;
A11: dom f = n by A8, FUNCT_2:def 1;
x in n by A9;
then reconsider x9 = x as Element of NAT by A7;
A12: x9 < n by A9, NAT_1:44;
A13: f . x9 = g . x9 by A2, A9, FUNCT_1:47;
not Segm k is empty by A8;
then not k is zero ;
then not k + l is zero ;
then not Segm (k + l) is empty ;
then A14: dom g = Segm (n + m) by FUNCT_2:def 1;
n <= n + m by NAT_1:11;
then A15: Segm n c= Segm (n + m) by NAT_1:39;

A16: now :: thesis: for n1 being Nat st n1 in f " {k1} holds
min* (g " {k1}) <= n1

let n1 be Nat; :: thesis: ( n1 in f " {k1} implies min* (g " {k1}) <= n1 )
assume A17: n1 in f " {k1} ; :: thesis: min* (g " {k1}) <= n1
A18: n1 in n by A11, A17, FUNCT_1:def 7;
f . n1 in {k1} by A17, FUNCT_1:def 7;
then g . n1 in {k1} by A2, A11, A18, FUNCT_1:47;
then n1 in g " {k1} by A14, A15, A18, FUNCT_1:def 7;
hence min* (g " {k1}) <= n1 by NAT_1:def 1; :: thesis: verum

end;

k1 in {k1} by TARSKI:def 1;
then A19: x9 in g " {k1} by A9, A10, A11, A14, A15, A13, FUNCT_1:def 7;
then min* (g " {k1}) <= x9 by NAT_1:def 1;
then min* (g " {k1}) < n by A12, XXREAL_0:2;
then A20: min* (g " {k1}) in dom f by A11, NAT_1:44;
min* (g " {k1}) in g " {k1} by A19, NAT_1:def 1;
then g . (min* (g " {k1})) in {k1} by FUNCT_1:def 7;
then f . (min* (g " {k1})) in {k1} by A2, A20, FUNCT_1:47;
then min* (g " {k1}) in f " {k1} by A20, FUNCT_1:def 7;
hence ( k1 in rng g & min* (f " {k1}) = min* (g " {k1}) ) by A9, A10, A11, A14, A15, A13, A16, FUNCT_1:def 3, NAT_1:def 1; :: thesis: verum

end;

A21: ( i in NAT & j in NAT ) by ORDINAL1:def 12;
then A22: j in rng g by A4, A6;
A23: min* (f " {j}) = min* (g " {j}) by A4, A6, A21;
A24: min* (f " {i}) = min* (g " {i}) by A3, A6, A21;
i in rng g by A3, A6, A21;
hence min* (f " {i}) < min* (f " {j}) by A1, A5, A22, A24, A23; :: thesis: verum