:: deftheorem defines CutLastLoc VALUED_1:def 18 :
for F being NAT -defined non empty finite Function holds CutLastLoc F = F \ ((LastLoc F) .--> (F . (LastLoc F)));