let n, k, m be 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 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 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 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 Nat st i in rng g & j in rng g & i < j holds
min* (g " {i}) < min* (g " {j})
A3: for i being Nat st i < n holds
f . i = g . i
proof
( k = 0 iff n = 0 ) by A1, Def1;
then A4: dom f = n by FUNCT_2:def 1;
let i be Nat; :: thesis: ( i < n implies f . i = g . i )
assume i < n ; :: thesis: f . i = g . i
then i in n by NAT_1:44;
hence f . i = g . i by A2, A4, FUNCT_1:47; :: thesis: verum
end;
A5: for l being Nat st l in rng g & not l in rng f holds
l = g . n
proof
A6: n + 1 is Subset of NAT by Th8;
let l be Nat; :: thesis: ( l in rng g & not l in rng f implies l = g . n )
assume that
A7: l in rng g and
A8: not l in rng f ; :: thesis: l = g . n
consider x being set such that
A9: x in dom g and
A10: g . x = l by A7, FUNCT_1:def 3;
assume A11: l <> g . n ; :: thesis: contradiction
dom g = n + 1 by A7, FUNCT_2:def 1;
then reconsider x = x as Element of NAT by A9, A6;
x < n + 1 by A9, NAT_1:44;
then x <= n by NAT_1:13;
then A12: x < n by A11, A10, XXREAL_0:1;
then A13: x in n by NAT_1:44;
k <> 0 by A1, A12, Def1;
then A14: dom f = n by FUNCT_2:def 1;
f . x = g . x by A3, A12;
hence contradiction by A8, A10, A14, A13, FUNCT_1:def 3; :: thesis: verum
end;
A15: for l being Nat st l in rng g & not l in rng f holds
min* (g " {l}) = n
proof
A16: n < n + 1 by NAT_1:13;
let l be Nat; :: thesis: ( l in rng g & not l in rng f implies min* (g " {l}) = n )
assume that
A17: l in rng g and
A18: not l in rng f ; :: thesis: min* (g " {l}) = n
A19: l in {l} by TARSKI:def 1;
dom g = n + 1 by A17, FUNCT_2:def 1;
then A20: n in dom g by A16, NAT_1:44;
g . n = l by A5, A17, A18;
then n in g " {l} by A20, A19, FUNCT_1:def 7;
then min* (g " {l}) in g " {l} by NAT_1:def 1;
then A21: g . (min* (g " {l})) in {l} by FUNCT_1:def 7;
assume A22: min* (g " {l}) <> n ; :: thesis: contradiction
min* (g " {l}) <= (n + 1) - 1 by Th16;
then A23: min* (g " {l}) < n by A22, XXREAL_0:1;
then k <> 0 by A1, Def1;
then A24: dom f = n by FUNCT_2:def 1;
min* (g " {l}) in n by A23, NAT_1:44;
then A25: f . (min* (g " {l})) in rng f by A24, FUNCT_1:def 3;
f . (min* (g " {l})) = g . (min* (g " {l})) by A3, A23;
hence contradiction by A18, A21, A25, TARSKI:def 1; :: thesis: verum
end;
A26: 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 A27: n c= n + 1 by NAT_1:39;
let k1 be Element of NAT ; :: thesis: ( k1 in rng f implies min* (g " {k1}) = min* (f " {k1}) )
assume A28: k1 in rng f ; :: thesis: min* (g " {k1}) = min* (f " {k1})
consider x being set such that
A29: x in dom f and
A30: f . x = k1 by A28, FUNCT_1:def 3;
A31: x in n by A29;
A32: dom g = n + 1 by A28, FUNCT_2:def 1;
n is Subset of NAT by Th8;
then reconsider x = x as Element of NAT by A31;
k1 in {k1} by TARSKI:def 1;
then A33: x in f " {k1} by A29, A30, FUNCT_1:def 7;
then A34: min* (f " {k1}) <= x by NAT_1:def 1;
A35: x < n by A29, NAT_1:44;
then A36: min* (f " {k1}) < n by A34, XXREAL_0:2;
A37: dom f = n by A28, FUNCT_2:def 1;
A38: now
let n1 be Nat; :: thesis: ( n1 in g " {k1} implies min* (f " {k1}) <= n1 )
assume A39: n1 in g " {k1} ; :: thesis: min* (f " {k1}) <= n1
n1 in n + 1 by A32, A39, FUNCT_1:def 7;
then n1 < n + 1 by NAT_1:44;
then A40: n1 <= n by NAT_1:13;
hence min* (f " {k1}) <= n1 ; :: thesis: verum
end;
min* (f " {k1}) in f " {k1} by A33, NAT_1:def 1;
then f . (min* (f " {k1})) in {k1} by FUNCT_1:def 7;
then A43: g . (min* (f " {k1})) in {k1} by A3, A36;
min* (f " {k1}) in n by A36, NAT_1:44;
then min* (f " {k1}) in g " {k1} by A32, A27, A43, FUNCT_1:def 7;
hence min* (g " {k1}) = min* (f " {k1}) by A38, NAT_1:def 1; :: thesis: verum
end;
let i, j be Nat; :: thesis: ( i in rng g & j in rng g & i < j implies min* (g " {i}) < min* (g " {j}) )
assume that
A44: i in rng g and
A45: j in rng g and
A46: i < j ; :: thesis: min* (g " {i}) < min* (g " {j})
A47: for l being Nat st l in rng g & not l in rng f holds
l >= k
proof
let l be Nat; :: thesis: ( l in rng g & not l in rng f implies l >= k )
assume that
l in rng g and
A48: not l in rng f ; :: thesis: l >= k
assume l < k ; :: thesis: contradiction
then l in k by NAT_1:44;
hence contradiction by A1, A48, FUNCT_2:def 3; :: thesis: verum
end;
A49: ( i in NAT & j in NAT ) by ORDINAL1:def 12;
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 A50: ( i in rng f & j in rng f ) ; :: thesis: min* (g " {i}) < min* (g " {j})
then A51: min* (g " {j}) = min* (f " {j}) by A26, A49;
min* (g " {i}) = min* (f " {i}) by A26, A50, A49;
hence min* (g " {i}) < min* (g " {j}) by A1, A46, A50, A51, Def1; :: thesis: verum
end;
suppose A52: ( i in rng f & not j in rng f ) ; :: thesis: min* (g " {i}) < min* (g " {j})
then A53: n <> 0 ;
then min* (f " {i}) <= n - 1 by Th16;
then A54: min* (g " {i}) <= n - 1 by A26, A52, A49;
n - 1 is Element of NAT by A53, NAT_1:20;
then A55: n - 1 < (n - 1) + 1 by NAT_1:13;
min* (g " {j}) = n by A45, A15, A52;
hence min* (g " {i}) < min* (g " {j}) by A54, A55, XXREAL_0:2; :: thesis: verum
end;
suppose A56: ( not i in rng f & j in rng f ) ; :: thesis: min* (g " {i}) < min* (g " {j})
then A57: j < k by NAT_1:44;
i >= k by A44, A47, A56;
hence min* (g " {i}) < min* (g " {j}) by A46, A57, XXREAL_0:2; :: thesis: verum
end;
suppose A58: ( not i in rng f & not j in rng f ) ; :: thesis: min* (g " {i}) < min* (g " {j})
then i = g . n by A44, A5;
hence min* (g " {i}) < min* (g " {j}) by A45, A46, A5, A58; :: thesis: verum
end;
end;
end;
hence min* (g " {i}) < min* (g " {j}) ; :: thesis: verum