let F be NAT -defined non empty finite Function; :: thesis: dom F = (dom (CutLastLoc F)) \/ {(LastLoc F)}
LastLoc F in dom F by Th31;
then A1: {(LastLoc F)} c= dom F by ZFMISC_1:31;
dom (CutLastLoc F) = (dom F) \ {(LastLoc F)} by Th37;
hence dom F = (dom (CutLastLoc F)) \/ {(LastLoc F)} by A1, XBOOLE_1:45; :: thesis: verum