let k be Nat; :: according to COMPOS_1:def 9 :: thesis: ( (stop p) . k = halt S & k in dom (stop p) implies k = LastLoc (stop p) )
assume that
Z1: (stop p) . k = halt S and
Z2: k in dom (stop p) ; :: thesis: k = LastLoc (stop p)
A: dom (stop p) = (dom (CutLastLoc (stop p))) \/ {(LastLoc (stop p))} by VALUED_1:37;

now

assume k in dom (CutLastLoc (stop p)) ; :: thesis: contradiction
then B: k in dom p by Th68;
then p . k = halt S by Th63, Z1;
hence contradiction by Def25, B; :: thesis: verum

end;

then k in {(LastLoc (stop p))} by Z2, A, XBOOLE_0:def 3;
hence k = LastLoc (stop p) by TARSKI:def 1; :: thesis: verum