let Ke, Ne be Subset of NAT; :: thesis: for F being Function of Ne,Ke st F is 'increasing holds

min* (rng F) = F . (min* (dom F))

let F be Function of Ne,Ke; :: thesis: ( F is 'increasing implies min* (rng F) = F . (min* (dom F)) )

assume A1: F is 'increasing ; :: thesis: min* (rng F) = F . (min* (dom F))

min* (rng F) = F . (min* (dom F))

let F be Function of Ne,Ke; :: thesis: ( F is 'increasing implies min* (rng F) = F . (min* (dom F)) )

assume A1: F is 'increasing ; :: thesis: min* (rng F) = F . (min* (dom F))

now :: thesis: min* (rng F) = F . (min* (dom F))end;

hence
min* (rng F) = F . (min* (dom F))
; :: thesis: verumper cases
( rng F is empty or not rng F is empty )
;

end;

suppose A2:
rng F is empty
; :: thesis: min* (rng F) = F . (min* (dom F))

then A3:
min* (rng F) = 0
by NAT_1:def 1;

dom F = {} by A2, RELAT_1:42;

hence min* (rng F) = F . (min* (dom F)) by A3, FUNCT_1:def 2; :: thesis: verum

end;dom F = {} by A2, RELAT_1:42;

hence min* (rng F) = F . (min* (dom F)) by A3, FUNCT_1:def 2; :: thesis: verum

suppose A4:
not rng F is empty
; :: thesis: min* (rng F) = F . (min* (dom F))

then reconsider rngF = rng F, Ke = Ke as non empty Subset of NAT by XBOOLE_1:1;

reconsider domF = dom F as non empty Subset of NAT by A4, FUNCT_2:def 1, RELAT_1:42;

set md = min* domF;

set mr = min* rngF;

min* rngF = F . (min* domF)

end;reconsider domF = dom F as non empty Subset of NAT by A4, FUNCT_2:def 1, RELAT_1:42;

set md = min* domF;

set mr = min* rngF;

min* rngF = F . (min* domF)

proof

hence
min* (rng F) = F . (min* (dom F))
; :: thesis: verum
A5:
min* domF in dom F
by NAT_1:def 1;

then F . (min* domF) in rngF by FUNCT_1:def 3;

then A6: min* rngF <= F . (min* domF) by NAT_1:def 1;

assume min* rngF <> F . (min* domF) ; :: thesis: contradiction

then A7: min* rngF < F . (min* domF) by A6, XXREAL_0:1;

A8: min* domF in domF by NAT_1:def 1;

A9: min* domF in dom F by NAT_1:def 1;

min* rngF in rngF by NAT_1:def 1;

then consider x being object such that

A10: x in dom F and

A11: F . x = min* rngF by FUNCT_1:def 3;

A12: F . (min* domF) in {(F . (min* domF))} by TARSKI:def 1;

F . x in {(min* rngF)} by A11, TARSKI:def 1;

then reconsider Fmr = F " {(min* rngF)}, Fmd = F " {(F . (min* domF))} as non empty Subset of NAT by A10, A12, A9, FUNCT_1:def 7, XBOOLE_1:1;

A13: min* rngF in rngF by NAT_1:def 1;

min* Fmr in Fmr by NAT_1:def 1;

then min* Fmr in domF by FUNCT_1:def 7;

then A14: min* Fmr >= min* domF by NAT_1:def 1;

F . (min* domF) in {(F . (min* domF))} by TARSKI:def 1;

then min* domF in Fmd by A8, FUNCT_1:def 7;

then A15: min* domF >= min* Fmd by NAT_1:def 1;

F . (min* domF) in rng F by A5, FUNCT_1:def 3;

then min* (F " {(min* rngF)}) < min* (F " {(F . (min* domF))}) by A1, A7, A13;

hence contradiction by A14, A15, XXREAL_0:2; :: thesis: verum

end;then F . (min* domF) in rngF by FUNCT_1:def 3;

then A6: min* rngF <= F . (min* domF) by NAT_1:def 1;

assume min* rngF <> F . (min* domF) ; :: thesis: contradiction

then A7: min* rngF < F . (min* domF) by A6, XXREAL_0:1;

A8: min* domF in domF by NAT_1:def 1;

A9: min* domF in dom F by NAT_1:def 1;

min* rngF in rngF by NAT_1:def 1;

then consider x being object such that

A10: x in dom F and

A11: F . x = min* rngF by FUNCT_1:def 3;

A12: F . (min* domF) in {(F . (min* domF))} by TARSKI:def 1;

F . x in {(min* rngF)} by A11, TARSKI:def 1;

then reconsider Fmr = F " {(min* rngF)}, Fmd = F " {(F . (min* domF))} as non empty Subset of NAT by A10, A12, A9, FUNCT_1:def 7, XBOOLE_1:1;

A13: min* rngF in rngF by NAT_1:def 1;

min* Fmr in Fmr by NAT_1:def 1;

then min* Fmr in domF by FUNCT_1:def 7;

then A14: min* Fmr >= min* domF by NAT_1:def 1;

F . (min* domF) in {(F . (min* domF))} by TARSKI:def 1;

then min* domF in Fmd by A8, FUNCT_1:def 7;

then A15: min* domF >= min* Fmd by NAT_1:def 1;

F . (min* domF) in rng F by A5, FUNCT_1:def 3;

then min* (F " {(min* rngF)}) < min* (F " {(F . (min* domF))}) by A1, A7, A13;

hence contradiction by A14, A15, XXREAL_0:2; :: thesis: verum