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

proof

let i be Element of NAT ; :: thesis: ( i < n implies f . i = g . i )
assume A4: i < n ; :: thesis: f . i = g . i
( k = 0 iff n = 0 ) by A1, Def1;
then ( i in n & dom f = n ) by A4, FUNCT_2:def 1, NAT_1:45;
hence f . i = g . i by A2, FUNCT_1:70; :: thesis: verum

end;

let i, j be Element of NAT ; :: thesis: ( i in rng g & j in rng g & i < j implies min* (g " {i}) < min* (g " {j}) )
assume A5: ( i in rng g & j in rng g & i < j ) ; :: thesis: min* (g " {i}) < min* (g " {j})
A6: for l being Element of NAT st l in rng g & not l in rng f holds
l = g . n

proof

let l be Element of NAT ; :: thesis: ( l in rng g & not l in rng f implies l = g . n )
assume A7: ( l in rng g & not l in rng f ) ; :: thesis: l = g . n
assume A8: l <> g . n ; :: thesis: contradiction
consider x being set such that
A9: ( x in dom g & g . x = l ) by A7, FUNCT_1:def 5;
( dom g = n + 1 & n + 1 is Subset of NAT ) by A7, Th8, FUNCT_2:def 1;
then reconsider x = x as Element of NAT by A9;
x < n + 1 by A9, NAT_1:45;
then x <= n by NAT_1:13;
then A10: x < n by A8, A9, XXREAL_0:1;
then k <> 0 by A1, Def1;
then ( dom f = n & x in n & f . x = g . x ) by A3, A10, FUNCT_2:def 1, NAT_1:45;
hence contradiction by A7, A9, FUNCT_1:def 5; :: thesis: verum

end;

A11: for l being Element of NAT st l in rng g & not l in rng f holds
min* (g " {l}) = n

proof

let l be Element of NAT ; :: thesis: ( l in rng g & not l in rng f implies min* (g " {l}) = n )
assume A12: ( l in rng g & not l in rng f ) ; :: thesis: min* (g " {l}) = n
assume A13: min* (g " {l}) <> n ; :: thesis: contradiction
( n < n + 1 & dom g = n + 1 ) by A12, FUNCT_2:def 1, NAT_1:13;
then ( n + 1 > 0 & n in dom g & l in {l} & g . n = l ) by A6, A12, NAT_1:45, TARSKI:def 1;
then ( min* (g " {l}) <= (n + 1) - 1 & n in g " {l} ) by Th16, FUNCT_1:def 13;
then A14: ( min* (g " {l}) < n & min* (g " {l}) in g " {l} ) by A13, NAT_1:def 1, XXREAL_0:1;
then A15: ( min* (g " {l}) in n & g . (min* (g " {l})) in {l} & 0 < n & f . (min* (g " {l})) = g . (min* (g " {l})) ) by A3, FUNCT_1:def 13, NAT_1:45;
k <> 0 by A1, A14, Def1;
then dom f = n by FUNCT_2:def 1;
then f . (min* (g " {l})) in rng f by A15, FUNCT_1:def 5;
hence contradiction by A12, A15, TARSKI:def 1; :: thesis: verum

end;

A16: for l being Element of NAT st l in rng g & not l in rng f holds
l >= k

proof

let l be Element of NAT ; :: thesis: ( l in rng g & not l in rng f implies l >= k )
assume A17: ( l in rng g & not l in rng f ) ; :: thesis: l >= k
assume l < k ; :: thesis: contradiction
then ( l in k & rng f = k ) by A1, FUNCT_2:def 3, NAT_1:45;
hence contradiction by A17; :: thesis: verum

end;

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

proof

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

now

let n1 be Nat; :: thesis: ( n1 in g " {k1} implies min* (f " {k1}) <= n1 )
assume A24: n1 in g " {k1} ; :: thesis: min* (f " {k1}) <= n1
n1 in n + 1 by A21, A24, FUNCT_1:def 13;
then n1 < n + 1 by NAT_1:45;
then A25: n1 <= n by NAT_1:13;

now

per cases ( n1 < n or n1 = n ) by A25, XXREAL_0:1;

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

then ( n1 < n & n1 in dom f & g . n1 in {k1} ) by A21, A24, FUNCT_1:def 13, NAT_1:45;
then ( f . n1 in {k1} & n1 in dom f ) by A3, A24;
then n1 in f " {k1} by FUNCT_1:def 13;
hence min* (f " {k1}) <= n1 by NAT_1:def 1; :: thesis: verum

end;

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

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

end;

end;

end;

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

end;

hence min* (g " {k1}) = min* (f " {k1}) by A23, NAT_1:def 1; :: thesis: verum

end;

now

per cases ( ( i in rng f & j in rng f ) or ( i in rng f & not j in rng f ) or ( not i in rng f & j in rng f ) or ( not i in rng f & not j in rng f ) ) ;

suppose A26: ( i in rng f & j in rng f ) ; :: thesis: min* (g " {i}) < min* (g " {j})

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

end;

suppose A27: ( i in rng f & not j in rng f ) ; :: thesis: min* (g " {i}) < min* (g " {j})

then n <> 0 ;
then ( min* (f " {i}) <= n - 1 & min* (g " {i}) = min* (f " {i}) & n - 1 is Element of NAT ) by A18, A27, Th16, NAT_1:20;
then ( min* (g " {i}) <= n - 1 & n - 1 < (n - 1) + 1 & min* (g " {j}) = n ) by A5, A11, A27, NAT_1:13;
hence min* (g " {i}) < min* (g " {j}) by XXREAL_0:2; :: thesis: verum

end;

suppose ( not i in rng f & j in rng f ) ; :: thesis: min* (g " {i}) < min* (g " {j})

then ( i >= k & j < k ) by A5, A16, NAT_1:45;
hence min* (g " {i}) < min* (g " {j}) by A5, XXREAL_0:2; :: thesis: verum

end;

suppose ( not i in rng f & not j in rng f ) ; :: thesis: min* (g " {i}) < min* (g " {j})

then ( i = g . n & j = g . n ) by A5, A6;
hence min* (g " {i}) < min* (g " {j}) by A5; :: thesis: verum

end;

end;

end;

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