theorem :: VALUED_1:33

for F being NAT -defined non empty finite Function holds FirstLoc F in dom F by XXREAL_2:def 7;