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