let Ne, Ke 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

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 dom F = {} by RELAT_1:65;
then ( min* (dom F) = 0 & min* (rng F) = 0 & F . 0 = 0 ) by A2, FUNCT_1:def 4, NAT_1:def 1;
hence min* (rng F) = F . (min* (dom F)) ; :: thesis: verum

end;

suppose A3: 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;
not Ke is empty ;
then reconsider domF = dom F as non empty Subset of NAT by A3, FUNCT_2:def 1, RELAT_1:65;
set md = min* domF;
set mr = min* rngF;
min* rngF = F . (min* domF)

proof

assume A4: min* rngF <> F . (min* domF) ; :: thesis: contradiction
A5: min* domF in dom F by NAT_1:def 1;
then F . (min* domF) in rngF by FUNCT_1:def 5;
then min* rngF <= F . (min* domF) by NAT_1:def 1;
then ( min* rngF < F . (min* domF) & min* rngF in rngF & F . (min* domF) in rng F ) by A4, A5, FUNCT_1:def 5, NAT_1:def 1, XXREAL_0:1;
then A6: min* (F " {(min* rngF)}) < min* (F " {(F . (min* domF))}) by A1, Def5;
min* rngF in rngF by NAT_1:def 1;
then consider x being set such that
A7: ( x in dom F & F . x = min* rngF ) by FUNCT_1:def 5;
( F . x in {(min* rngF)} & F . (min* domF) in {(F . (min* domF))} & min* domF in dom F ) by A7, NAT_1:def 1, TARSKI:def 1;
then reconsider Fmr = F " {(min* rngF)}, Fmd = F " {(F . (min* domF))} as non empty Subset of NAT by A7, FUNCT_1:def 13, XBOOLE_1:1;
( min* Fmr in Fmr & F . (min* domF) in {(F . (min* domF))} & min* domF in domF ) by NAT_1:def 1, TARSKI:def 1;
then ( min* Fmr in domF & min* domF in Fmd ) by FUNCT_1:def 13;
then ( min* Fmr >= min* domF & min* domF >= min* Fmd ) by NAT_1:def 1;
hence contradiction by A6, 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