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))

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

per cases ( rng F is empty or not rng F is empty ) ;

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;

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)

proof

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;

hence min* (rng F) = F . (min* (dom F)) ; :: thesis: verum

end;

end;

end;

hence min* (rng F) = F . (min* (dom F)) ; :: thesis: verum