let F be non empty NAT -defined finite Function; :: thesis: not LastLoc F in dom (CutLastLoc F)
LastLoc F in dom F by VALUED_1:30;
then F | {(LastLoc F)} = (LastLoc F) .--> (F . (LastLoc F)) by FUNCT_7:6;
then A1: dom (CutLastLoc F) = (dom F) \ {(LastLoc F)} by RELAT_1:177;
LastLoc F in {(LastLoc F)} by TARSKI:def 1;
hence not LastLoc F in dom (CutLastLoc F) by A1, XBOOLE_0:def 5; :: thesis: verum