let k be Nat; :: according to COMPOS_1:def 15 :: thesis: ( (stop p) . k = halt S & k in dom (stop p) implies k = LastLoc (stop p) )
assume that
A1: (stop p) . k = halt S and
A2: k in dom (stop p) ; :: thesis: k = LastLoc (stop p)
A3: dom (stop p) = (dom (CutLastLoc (stop p))) \/ {(LastLoc (stop p))} by VALUED_1:37;
now :: thesis: not k in dom (CutLastLoc (stop p))
assume k in dom (CutLastLoc (stop p)) ; :: thesis: contradiction
then A4: k in dom p ;
then p . k = halt S by A1, AFINSQ_1:def 3;
hence contradiction by Def14, A4; :: thesis: verum
end;
then k in {(LastLoc (stop p))} by A2, A3, XBOOLE_0:def 3;
hence k = LastLoc (stop p) by TARSKI:def 1; :: thesis: verum