let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite standard AMI-Struct of N
for F being NAT -defined non empty FinPartState of holds dom F = (dom (CutLastLoc F)) \/ {(LastLoc F)}
let S be non empty stored-program IC-Ins-separated definite standard AMI-Struct of N; :: thesis: for F being NAT -defined non empty FinPartState of holds dom F = (dom (CutLastLoc F)) \/ {(LastLoc F)}
let F be NAT -defined non empty FinPartState of ; :: thesis: dom F = (dom (CutLastLoc F)) \/ {(LastLoc F)}
LastLoc F in dom F by AMISTD_1:51;
then A1: {(LastLoc F)} c= dom F by ZFMISC_1:37;
dom (CutLastLoc F) = (dom F) \ {(LastLoc F)} by Th47;
hence dom F = (dom (CutLastLoc F)) \/ {(LastLoc F)} by A1, XBOOLE_1:45; :: thesis: verum