theorem :: AFINSQ_1:71

for F being NAT -defined non empty finite initial Function holds FirstLoc F = 0 by Th62, VALUED_1:35;