theorem :: VALUED_1:30

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