theorem Th35: :: VALUED_1:36

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