let F be NAT -defined non empty finite initial Function; :: thesis: FirstLoc F = 0
0 in dom F by Th69;
then FirstLoc F <= 0 by VALUED_1:36;
hence FirstLoc F = 0 ; :: thesis: verum