let F be NAT -defined non empty finite Function; :: thesis: dom (CutLastLoc F) = (dom F) \ {(LastLoc F)}
A1: dom ((LastLoc F) .--> (F . (LastLoc F))) = {(LastLoc F)} by FUNCOP_1:13;
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)} by FUNCOP_1:13;
thus dom (CutLastLoc F) c= (dom F) \ {(LastLoc F)} :: according to XBOOLE_0:def 10 :: thesis: (dom F) \ {(LastLoc F)} c= dom (CutLastLoc F)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in dom (CutLastLoc F) or x in (dom F) \ {(LastLoc F)} )
assume x in dom (CutLastLoc F) ; :: thesis: x in (dom F) \ {(LastLoc F)}
then consider y being set such that
A4: [x,y] in F \ R by A2, RELAT_1:def 4;
A5: not [x,y] in R by A4, XBOOLE_0:def 5;
A6: x in dom F by A4, RELAT_1:def 4;

per cases ( x <> LastLoc F or y <> F . (LastLoc F) ) by A5, TARSKI:def 1;

suppose x <> LastLoc F ; :: thesis: x in (dom F) \ {(LastLoc F)}

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

end;

suppose A7: y <> F . (LastLoc F) ; :: thesis: x in (dom F) \ {(LastLoc F)}

now

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

end;

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

end;

end;

end;

thus (dom F) \ {(LastLoc F)} c= dom (CutLastLoc F) by A1, RELAT_1:3; :: thesis: verum