let F be NAT -defined non empty finite Function; :: thesis: FirstLoc F in dom F
set M = dom F;
min (dom F) in dom F by XXREAL_2:def 7;
hence FirstLoc F in dom F ; :: thesis: verum