theorem :: VALUED_1:37

for F being NAT -defined non empty finite Function holds dom F = (dom (CutLastLoc F)) \/ {(LastLoc F)}