theorem :: VALUED_1:35

for l1 being Element of NAT
for F being NAT -defined non empty finite Function st l1 in dom F holds
FirstLoc F <= l1 by XXREAL_2:def 7;