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 ;
hence min* (rng F) = F . (min* (dom F)) by ; :: 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 ;
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 ;
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 ;
then reconsider Fmr = F " {(min* rngF)}, Fmd = F " {(F . (min* domF))} as non empty Subset of NAT by ;
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 ;
then A15: min* domF >= min* Fmd by NAT_1:def 1;
F . (min* domF) in rng F by ;
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