let N be with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite standard AMI-Struct of NAT ,N
for F being non empty programmed FinPartState of S holds dom (CutLastLoc F) = (dom F) \ {(LastLoc F)}
let S be non empty stored-program IC-Ins-separated definite standard AMI-Struct of NAT ,N; :: thesis: for F being non empty programmed FinPartState of S holds dom (CutLastLoc F) = (dom F) \ {(LastLoc F)}
let F be non empty programmed FinPartState of S; :: thesis: dom (CutLastLoc F) = (dom F) \ {(LastLoc F)}
A1: dom ((LastLoc F) .--> (F . (LastLoc F))) = {(LastLoc F)} by FUNCOP_1:19;
reconsider R = {[(LastLoc F),(F . (LastLoc F))]} as Relation ;
A2: R = (LastLoc F) .--> (F . (LastLoc F)) by FUNCT_4:87;
then A3: dom R = {(LastLoc F)} by FUNCOP_1:19;
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: ( [x,y] in F & 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:8; :: 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:15; :: thesis: verum