let F be NAT -defined non empty finite Function; :: thesis:
A1: dom ((LastLoc F) .--> (F . (LastLoc F))) = {(LastLoc F)} ;
reconsider R = {[(LastLoc F),(F . (LastLoc F))]} as Relation ;
A2: R = (LastLoc F) .--> (F . (LastLoc F)) by FUNCT_4:82;
then A3: dom R = {(LastLoc F)} ;
thus dom (CutLastLoc F) c= (dom F) \ {(LastLoc F)} :: according to XBOOLE_0:def 10 :: thesis:

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in dom (CutLastLoc F) ; :: thesis:
then consider y being object such that
A4: [x,y] in F \ R by A2, XTUPLE_0:def 12;
A5: not [x,y] in R by A4, XBOOLE_0:def 5;
A6: x in dom F by A4, XTUPLE_0:def 12;

per cases by A5, TARSKI:def 1;

suppose x <> LastLoc F ; :: thesis:

then not x in dom R by A3, TARSKI:def 1;
hence x in (dom F) \ {(LastLoc F)} by A2, A6, XBOOLE_0:def 5; :: thesis:

end;

suppose A7: y <> F . (LastLoc F) ; :: thesis:

assume x in dom R ; :: thesis:
then x = LastLoc F by A3, TARSKI:def 1;
hence contradiction by A4, A7, FUNCT_1:1; :: thesis:

end;

hence x in (dom F) \ {(LastLoc F)} by A2, A6, XBOOLE_0:def 5; :: thesis:

end;

end;

end;

thus (dom F) \ {(LastLoc F)} c= dom (CutLastLoc F) by A1, XTUPLE_0:25; :: thesis: