let k, l, m, n be Nat; :: thesis: for f being Function of (Segm n),(Segm k)

for g being Function of (Segm (n + m)),(Segm (k + l)) st g is "increasing & f = g | n holds

for i, j being Nat st i in rng f & j in rng f & i < j holds

min* (f " {i}) < min* (f " {j})

let f be Function of (Segm n),(Segm k); :: thesis: for g being Function of (Segm (n + m)),(Segm (k + l)) st g is "increasing & f = g | n holds

for i, j being Nat st i in rng f & j in rng f & i < j holds

min* (f " {i}) < min* (f " {j})

let g be Function of (Segm (n + m)),(Segm (k + l)); :: thesis: ( g is "increasing & f = g | n implies for i, j being 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 Nat st i in rng f & j in rng f & i < j holds

min* (f " {i}) < min* (f " {j})

let i, j be Nat; :: thesis: ( i in rng f & j in rng f & i < j implies min* (f " {i}) < min* (f " {j}) )

assume that

A3: i in rng f and

A4: j in rng f and

A5: i < j ; :: thesis: min* (f " {i}) < min* (f " {j})

A6: for k1 being Element of NAT st k1 in rng f holds

( k1 in rng g & min* (f " {k1}) = min* (g " {k1}) )

then A22: j in rng g by A4, A6;

A23: min* (f " {j}) = min* (g " {j}) by A4, A6, A21;

A24: min* (f " {i}) = min* (g " {i}) by A3, A6, A21;

i in rng g by A3, A6, A21;

hence min* (f " {i}) < min* (f " {j}) by A1, A5, A22, A24, A23; :: thesis: verum

for g being Function of (Segm (n + m)),(Segm (k + l)) st g is "increasing & f = g | n holds

for i, j being Nat st i in rng f & j in rng f & i < j holds

min* (f " {i}) < min* (f " {j})

let f be Function of (Segm n),(Segm k); :: thesis: for g being Function of (Segm (n + m)),(Segm (k + l)) st g is "increasing & f = g | n holds

for i, j being Nat st i in rng f & j in rng f & i < j holds

min* (f " {i}) < min* (f " {j})

let g be Function of (Segm (n + m)),(Segm (k + l)); :: thesis: ( g is "increasing & f = g | n implies for i, j being 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 Nat st i in rng f & j in rng f & i < j holds

min* (f " {i}) < min* (f " {j})

let i, j be Nat; :: thesis: ( i in rng f & j in rng f & i < j implies min* (f " {i}) < min* (f " {j}) )

assume that

A3: i in rng f and

A4: j in rng f and

A5: i < j ; :: thesis: min* (f " {i}) < min* (f " {j})

A6: for k1 being Element of NAT st k1 in rng f holds

( k1 in rng g & min* (f " {k1}) = min* (g " {k1}) )

proof

A21:
( i in NAT & j in NAT )
by ORDINAL1:def 12;
A7:
n is Subset of NAT
by Th8;

let k1 be Element of NAT ; :: thesis: ( k1 in rng f implies ( k1 in rng g & min* (f " {k1}) = min* (g " {k1}) ) )

assume A8: k1 in rng f ; :: thesis: ( k1 in rng g & min* (f " {k1}) = min* (g " {k1}) )

consider x being object such that

A9: x in dom f and

A10: f . x = k1 by A8, FUNCT_1:def 3;

A11: dom f = n by A8, FUNCT_2:def 1;

x in n by A9;

then reconsider x9 = x as Element of NAT by A7;

A12: x9 < n by A9, NAT_1:44;

A13: f . x9 = g . x9 by A2, A9, FUNCT_1:47;

not Segm k is empty by A8;

then not k is zero ;

then not k + l is zero ;

then not Segm (k + l) is empty ;

then A14: dom g = Segm (n + m) by FUNCT_2:def 1;

n <= n + m by NAT_1:11;

then A15: Segm n c= Segm (n + m) by NAT_1:39;

then A19: x9 in g " {k1} by A9, A10, A11, A14, A15, A13, FUNCT_1:def 7;

then min* (g " {k1}) <= x9 by NAT_1:def 1;

then min* (g " {k1}) < n by A12, XXREAL_0:2;

then A20: min* (g " {k1}) in dom f by A11, NAT_1:44;

min* (g " {k1}) in g " {k1} by A19, NAT_1:def 1;

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

then f . (min* (g " {k1})) in {k1} by A2, A20, FUNCT_1:47;

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

hence ( k1 in rng g & min* (f " {k1}) = min* (g " {k1}) ) by A9, A10, A11, A14, A15, A13, A16, FUNCT_1:def 3, NAT_1:def 1; :: thesis: verum

end;let k1 be Element of NAT ; :: thesis: ( k1 in rng f implies ( k1 in rng g & min* (f " {k1}) = min* (g " {k1}) ) )

assume A8: k1 in rng f ; :: thesis: ( k1 in rng g & min* (f " {k1}) = min* (g " {k1}) )

consider x being object such that

A9: x in dom f and

A10: f . x = k1 by A8, FUNCT_1:def 3;

A11: dom f = n by A8, FUNCT_2:def 1;

x in n by A9;

then reconsider x9 = x as Element of NAT by A7;

A12: x9 < n by A9, NAT_1:44;

A13: f . x9 = g . x9 by A2, A9, FUNCT_1:47;

not Segm k is empty by A8;

then not k is zero ;

then not k + l is zero ;

then not Segm (k + l) is empty ;

then A14: dom g = Segm (n + m) by FUNCT_2:def 1;

n <= n + m by NAT_1:11;

then A15: Segm n c= Segm (n + m) by NAT_1:39;

A16: now :: thesis: for n1 being Nat st n1 in f " {k1} holds

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

k1 in {k1}
by TARSKI:def 1;min* (g " {k1}) <= n1

let n1 be Nat; :: thesis: ( n1 in f " {k1} implies min* (g " {k1}) <= n1 )

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

A18: n1 in n by A11, A17, FUNCT_1:def 7;

f . n1 in {k1} by A17, FUNCT_1:def 7;

then g . n1 in {k1} by A2, A11, A18, FUNCT_1:47;

then n1 in g " {k1} by A14, A15, A18, FUNCT_1:def 7;

hence min* (g " {k1}) <= n1 by NAT_1:def 1; :: thesis: verum

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

A18: n1 in n by A11, A17, FUNCT_1:def 7;

f . n1 in {k1} by A17, FUNCT_1:def 7;

then g . n1 in {k1} by A2, A11, A18, FUNCT_1:47;

then n1 in g " {k1} by A14, A15, A18, FUNCT_1:def 7;

hence min* (g " {k1}) <= n1 by NAT_1:def 1; :: thesis: verum

then A19: x9 in g " {k1} by A9, A10, A11, A14, A15, A13, FUNCT_1:def 7;

then min* (g " {k1}) <= x9 by NAT_1:def 1;

then min* (g " {k1}) < n by A12, XXREAL_0:2;

then A20: min* (g " {k1}) in dom f by A11, NAT_1:44;

min* (g " {k1}) in g " {k1} by A19, NAT_1:def 1;

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

then f . (min* (g " {k1})) in {k1} by A2, A20, FUNCT_1:47;

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

hence ( k1 in rng g & min* (f " {k1}) = min* (g " {k1}) ) by A9, A10, A11, A14, A15, A13, A16, FUNCT_1:def 3, NAT_1:def 1; :: thesis: verum

then A22: j in rng g by A4, A6;

A23: min* (f " {j}) = min* (g " {j}) by A4, A6, A21;

A24: min* (f " {i}) = min* (g " {i}) by A3, A6, A21;

i in rng g by A3, A6, A21;

hence min* (f " {i}) < min* (f " {j}) by A1, A5, A22, A24, A23; :: thesis: verum