let k, m, n be Nat; :: thesis: for f being Function of (Segm n),(Segm k)
for g being Function of (Segm (n + 1)),(Segm (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 (Segm n),(Segm k); :: thesis: for g being Function of (Segm (n + 1)),(Segm (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 (Segm (n + 1)),(Segm (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;
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 Segm n by NAT_1:44;
hence f . i = g . i by ; :: thesis: verum
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: ( l in rng g & not l in rng f implies l = g . n )
assume that
A6: l in rng g and
A7: not l in rng f ; :: thesis: l = g . n
consider x being object such that
A8: x in dom g and
A9: g . x = l by ;
assume A10: l <> g . n ; :: thesis: contradiction
dom g = n + 1 by ;
then reconsider x = x as Element of NAT by A8;
x < n + 1 by ;
then x <= n by NAT_1:13;
then A11: x < n by ;
then A12: x in Segm n by NAT_1:44;
k <> 0 by ;
then A13: dom f = n by FUNCT_2:def 1;
f . x = g . x by ;
hence contradiction by A7, A9, A13, A12, FUNCT_1:def 3; :: thesis: verum
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: ( l in rng g & not l in rng f implies min* (g " {l}) = n )
assume that
A16: l in rng g and
A17: not l in rng f ; :: thesis: min* (g " {l}) = n
A18: l in {l} by TARSKI:def 1;
dom g = n + 1 by ;
then A19: n in dom g by ;
g . n = l by A5, A16, A17;
then n in g " {l} by ;
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: contradiction
min* (g " {l}) <= (n + 1) - 1 by Th16;
then A22: min* (g " {l}) < n by ;
then k <> 0 by A1;
then A23: dom f = n by FUNCT_2:def 1;
min* (g " {l}) in Segm n by ;
then A24: f . (min* (g " {l})) in rng f by ;
f . (min* (g " {l})) = g . (min* (g " {l})) by ;
hence contradiction by A17, A20, A24, TARSKI:def 1; :: thesis: verum
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: ( k1 in rng f implies min* (g " {k1}) = min* (f " {k1}) )
assume A27: k1 in rng f ; :: thesis: min* (g " {k1}) = min* (f " {k1})
consider x being object such that
A28: x in dom f and
A29: f . x = k1 by ;
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 ;
then A33: min* (f " {k1}) <= x by NAT_1:def 1;
A34: x < n by ;
then A35: min* (f " {k1}) < n by ;
A36: dom f = n by ;
A37: now :: thesis: for n1 being Nat st n1 in g " {k1} holds
min* (f " {k1}) <= n1
let n1 be Nat; :: thesis: ( n1 in g " {k1} implies min* (f " {k1}) <= n1 )
assume A38: n1 in g " {k1} ; :: thesis: min* (f " {k1}) <= n1
n1 in Segm (n + 1) by ;
then n1 < n + 1 by NAT_1:44;
then A39: n1 <= n by NAT_1:13;
now :: thesis: min* (f " {k1}) <= n1
per cases ( n1 < n or n1 = n ) by ;
suppose A40: n1 < n ; :: thesis: min* (f " {k1}) <= n1
g . n1 in {k1} by ;
then A41: f . n1 in {k1} by ;
n1 in dom f by ;
then n1 in f " {k1} by ;
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 ; :: thesis: verum
end;
end;
end;
hence min* (f " {k1}) <= n1 ; :: thesis: verum
end;
min* (f " {k1}) in f " {k1} by ;
then f . (min* (f " {k1})) in {k1} by FUNCT_1:def 7;
then A42: g . (min* (f " {k1})) in {k1} by ;
min* (f " {k1}) in n by ;
then min* (f " {k1}) in g " {k1} by ;
hence min* (g " {k1}) = min* (f " {k1}) by ; :: 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
A43: i in rng g and
A44: j in rng g and
A45: i < j ; :: thesis: min* (g " {i}) < min* (g " {j})
A46: 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
A47: not l in rng f ; :: thesis: l >= k
assume l < k ; :: thesis: contradiction
then l in Segm k by NAT_1:44;
hence contradiction by A1, A47, FUNCT_2:def 3; :: thesis: verum
end;
A48: ( i in NAT & j in NAT ) by ORDINAL1:def 12;
now :: thesis: min* (g " {i}) < min* (g " {j})
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 A49: ( i in rng f & j in rng f ) ; :: thesis: min* (g " {i}) < min* (g " {j})
then A50: min* (g " {j}) = min* (f " {j}) by ;
min* (g " {i}) = min* (f " {i}) by ;
hence min* (g " {i}) < min* (g " {j}) by A1, A45, A49, A50; :: thesis: verum
end;
suppose A51: ( i in rng f & not j in rng f ) ; :: thesis: min* (g " {i}) < min* (g " {j})
then A52: n <> 0 ;
then min* (f " {i}) <= n - 1 by Th16;
then A53: min* (g " {i}) <= n - 1 by ;
n - 1 is Element of NAT by ;
then A54: n - 1 < (n - 1) + 1 by NAT_1:13;
min* (g " {j}) = n by ;
hence min* (g " {i}) < min* (g " {j}) by ; :: thesis: verum
end;
suppose A55: ( not i in rng f & j in rng f ) ; :: thesis: min* (g " {i}) < min* (g " {j})
then A56: j < k by NAT_1:44;
i >= k by ;
hence min* (g " {i}) < min* (g " {j}) by ; :: thesis: verum
end;
suppose A57: ( not i in rng f & not j in rng f ) ; :: thesis: min* (g " {i}) < min* (g " {j})
then i = g . n by ;
hence min* (g " {i}) < min* (g " {j}) by A44, A45, A5, A57; :: thesis: verum
end;
end;
end;
hence min* (g " {i}) < min* (g " {j}) ; :: thesis: verum