let n, k, m, l be Element of NAT ; :: thesis: for f being Function of n,k
for g being Function of (n + m),(k + l) st g is "increasing & f = g | n holds
for i, j being Element of NAT st i in rng f & j in rng f & i < j holds
min* (f " {i}) < min* (f " {j})
let f be Function of n,k; :: thesis: for g being Function of (n + m),(k + l) st g is "increasing & f = g | n holds
for i, j being Element of NAT st i in rng f & j in rng f & i < j holds
min* (f " {i}) < min* (f " {j})
let g be Function of (n + m),(k + l); :: thesis: ( g is "increasing & f = g | n implies for i, j being Element of 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 Element of NAT st i in rng f & j in rng f & i < j holds
min* (f " {i}) < min* (f " {j})
let i, j be Element of NAT ; :: thesis: ( i in rng f & j in rng f & i < j implies min* (f " {i}) < min* (f " {j}) )
assume A3: ( i in rng f & j in rng f & i < j ) ; :: thesis: min* (f " {i}) < min* (f " {j})
for k1 being Element of NAT st k1 in rng f holds
( k1 in rng g & min* (f " {k1}) = min* (g " {k1}) )

proof

let k1 be Element of NAT ; :: thesis: ( k1 in rng f implies ( k1 in rng g & min* (f " {k1}) = min* (g " {k1}) ) )
assume A4: k1 in rng f ; :: thesis: ( k1 in rng g & min* (f " {k1}) = min* (g " {k1}) )
consider x being set such that
A5: ( x in dom f & f . x = k1 ) by A4, FUNCT_1:def 5;
k <= k + l by NAT_1:11;
then k c= k + l by NAT_1:40;
then ( k1 in k & k1 in k + l & n <= n + m ) by A4, NAT_1:11, TARSKI:def 3;
then A6: ( dom f = n & dom g = n + m & n c= n + m ) by FUNCT_2:def 1, NAT_1:40;
( x in n & n is Subset of NAT ) by A5, Th8;
then reconsider x' = x as Element of NAT ;
A7: ( f . x' = g . x' & f . x' = k1 & k1 in {k1} & x' in dom g ) by A2, A5, A6, FUNCT_1:70, TARSKI:def 1;
then ( x' in f " {k1} & x' in g " {k1} & k1 in rng g ) by A5, FUNCT_1:def 5, FUNCT_1:def 13;
then ( min* (g " {k1}) <= x' & x' < n & min* (g " {k1}) in g " {k1} ) by A5, NAT_1:45, NAT_1:def 1;
then ( min* (g " {k1}) < n & g . (min* (g " {k1})) in {k1} ) by FUNCT_1:def 13, XXREAL_0:2;
then ( min* (g " {k1}) in dom f & g . (min* (g " {k1})) in {k1} ) by A6, NAT_1:45;
then ( min* (g " {k1}) in n & f . (min* (g " {k1})) in {k1} ) by A2, FUNCT_1:70;
then A8: min* (g " {k1}) in f " {k1} by A6, FUNCT_1:def 13;

now

let n1 be Nat; :: thesis: ( n1 in f " {k1} implies min* (g " {k1}) <= n1 )
assume A9: n1 in f " {k1} ; :: thesis: min* (g " {k1}) <= n1
n1 in n by A6, A9, FUNCT_1:def 13;
then ( n1 in dom f & n1 in dom g & f . n1 in {k1} ) by A6, A9, FUNCT_1:def 13;
then ( g . n1 in {k1} & n1 in dom g ) by A2, FUNCT_1:70;
then n1 in g " {k1} by FUNCT_1:def 13;
hence min* (g " {k1}) <= n1 by NAT_1:def 1; :: thesis: verum

end;

hence ( k1 in rng g & min* (f " {k1}) = min* (g " {k1}) ) by A7, A8, FUNCT_1:def 5, NAT_1:def 1; :: thesis: verum

end;

then ( i in rng g & j in rng g & min* (f " {i}) = min* (g " {i}) & min* (f " {j}) = min* (g " {j}) ) by A3;
hence min* (f " {i}) < min* (f " {j}) by A1, A3, Def1; :: thesis: verum