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