theorem Th62: :: STIRL2_1:62

for Ke, Ne being Subset of NAT
for F being Function of Ne,Ke st F is 'increasing holds
min* (rng F) = F . (min* (dom F))