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

l = g . n

min* (g " {l}) = n

min* (g " {k1}) = min* (f " {k1})

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

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

A5:
for l being Nat st l in rng g & not l in rng f holds
( 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 A2, A4, FUNCT_1:47; :: thesis: verum

end;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 A2, A4, FUNCT_1:47; :: thesis: verum

l = g . n

proof

A14:
for l being Nat st l in rng g & not l in rng f holds
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 A6, FUNCT_1:def 3;

assume A10: l <> g . n ; :: thesis: contradiction

dom g = n + 1 by A6, FUNCT_2:def 1;

then reconsider x = x as Element of NAT by A8;

x < n + 1 by A8, NAT_1:44;

then x <= n by NAT_1:13;

then A11: x < n by A10, A9, XXREAL_0:1;

then A12: x in Segm n by NAT_1:44;

k <> 0 by A1, A11;

then A13: dom f = n by FUNCT_2:def 1;

f . x = g . x by A3, A11;

hence contradiction by A7, A9, A13, A12, FUNCT_1:def 3; :: thesis: verum

end;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 A6, FUNCT_1:def 3;

assume A10: l <> g . n ; :: thesis: contradiction

dom g = n + 1 by A6, FUNCT_2:def 1;

then reconsider x = x as Element of NAT by A8;

x < n + 1 by A8, NAT_1:44;

then x <= n by NAT_1:13;

then A11: x < n by A10, A9, XXREAL_0:1;

then A12: x in Segm n by NAT_1:44;

k <> 0 by A1, A11;

then A13: dom f = n by FUNCT_2:def 1;

f . x = g . x by A3, A11;

hence contradiction by A7, A9, A13, A12, FUNCT_1:def 3; :: thesis: verum

min* (g " {l}) = n

proof

A25:
for k1 being Element of NAT st k1 in rng f holds
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 A16, FUNCT_2:def 1;

then A19: n in dom g by A15, NAT_1:44;

g . n = l by A5, A16, A17;

then n in g " {l} by A19, A18, FUNCT_1:def 7;

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 A21, XXREAL_0:1;

then k <> 0 by A1;

then A23: dom f = n by FUNCT_2:def 1;

min* (g " {l}) in Segm n by A22, NAT_1:44;

then A24: f . (min* (g " {l})) in rng f by A23, FUNCT_1:def 3;

f . (min* (g " {l})) = g . (min* (g " {l})) by A3, A22;

hence contradiction by A17, A20, A24, TARSKI:def 1; :: thesis: verum

end;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 A16, FUNCT_2:def 1;

then A19: n in dom g by A15, NAT_1:44;

g . n = l by A5, A16, A17;

then n in g " {l} by A19, A18, FUNCT_1:def 7;

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 A21, XXREAL_0:1;

then k <> 0 by A1;

then A23: dom f = n by FUNCT_2:def 1;

min* (g " {l}) in Segm n by A22, NAT_1:44;

then A24: f . (min* (g " {l})) in rng f by A23, FUNCT_1:def 3;

f . (min* (g " {l})) = g . (min* (g " {l})) by A3, A22;

hence contradiction by A17, A20, A24, TARSKI:def 1; :: thesis: verum

min* (g " {k1}) = min* (f " {k1})

proof

let i, j be Nat; :: thesis: ( i in rng g & j in rng g & i < j implies min* (g " {i}) < min* (g " {j}) )
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 A27, FUNCT_1:def 3;

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 A28, A29, FUNCT_1:def 7;

then A33: min* (f " {k1}) <= x by NAT_1:def 1;

A34: x < n by A28, NAT_1:44;

then A35: min* (f " {k1}) < n by A33, XXREAL_0:2;

A36: dom f = n by A27, FUNCT_2:def 1;

then f . (min* (f " {k1})) in {k1} by FUNCT_1:def 7;

then A42: g . (min* (f " {k1})) in {k1} by A3, A35;

min* (f " {k1}) in n by A35, NAT_1:44;

then min* (f " {k1}) in g " {k1} by A31, A26, A42, FUNCT_1:def 7;

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

end;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 A27, FUNCT_1:def 3;

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 A28, A29, FUNCT_1:def 7;

then A33: min* (f " {k1}) <= x by NAT_1:def 1;

A34: x < n by A28, NAT_1:44;

then A35: min* (f " {k1}) < n by A33, XXREAL_0:2;

A36: dom f = n by A27, FUNCT_2:def 1;

A37: now :: thesis: for n1 being Nat st n1 in g " {k1} holds

min* (f " {k1}) <= n1

min* (f " {k1}) in f " {k1}
by A32, NAT_1:def 1;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 A31, A38, FUNCT_1:def 7;

then n1 < n + 1 by NAT_1:44;

then A39: n1 <= n by NAT_1:13;

end;assume A38: n1 in g " {k1} ; :: thesis: min* (f " {k1}) <= n1

n1 in Segm (n + 1) by A31, A38, FUNCT_1:def 7;

then n1 < n + 1 by NAT_1:44;

then A39: n1 <= n by NAT_1:13;

now :: thesis: min* (f " {k1}) <= n1end;

hence
min* (f " {k1}) <= n1
; :: thesis: verumper cases
( n1 < n or n1 = n )
by A39, XXREAL_0:1;

end;

then f . (min* (f " {k1})) in {k1} by FUNCT_1:def 7;

then A42: g . (min* (f " {k1})) in {k1} by A3, A35;

min* (f " {k1}) in n by A35, NAT_1:44;

then min* (f " {k1}) in g " {k1} by A31, A26, A42, FUNCT_1:def 7;

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

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

A48:
( i in NAT & j in NAT )
by ORDINAL1:def 12;
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;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

now :: thesis: min* (g " {i}) < min* (g " {j})end;

hence
min* (g " {i}) < min* (g " {j})
; :: thesis: verumper 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 ) )
;

end;

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 A25, A48;

min* (g " {i}) = min* (f " {i}) by A25, A49, A48;

hence min* (g " {i}) < min* (g " {j}) by A1, A45, A49, A50; :: thesis: verum

end;min* (g " {i}) = min* (f " {i}) by A25, A49, A48;

hence min* (g " {i}) < min* (g " {j}) by A1, A45, A49, A50; :: thesis: verum

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 A25, A51, A48;

n - 1 is Element of NAT by A52, NAT_1:20;

then A54: n - 1 < (n - 1) + 1 by NAT_1:13;

min* (g " {j}) = n by A44, A14, A51;

hence min* (g " {i}) < min* (g " {j}) by A53, A54, XXREAL_0:2; :: thesis: verum

end;then min* (f " {i}) <= n - 1 by Th16;

then A53: min* (g " {i}) <= n - 1 by A25, A51, A48;

n - 1 is Element of NAT by A52, NAT_1:20;

then A54: n - 1 < (n - 1) + 1 by NAT_1:13;

min* (g " {j}) = n by A44, A14, A51;

hence min* (g " {i}) < min* (g " {j}) by A53, A54, XXREAL_0:2; :: thesis: verum