thus (Stop S) . (LastLoc (Stop S)) = ((il. S,0 ) .--> (halt S)) . (il. S,0 ) by Th27
.= halt S by FUNCOP_1:87 ; :: according to AMISTD_1:def 22 :: thesis: Stop S is unique-halt
let l be Instruction-Location of S; :: according to AMISTD_1:def 23 :: thesis: ( not (Stop S) . l = halt S or not l in dom (Stop S) or l = LastLoc (Stop S) )
assume (Stop S) . l = halt S ; :: thesis: ( not l in dom (Stop S) or l = LastLoc (Stop S) )
assume l in dom (Stop S) ; :: thesis: l = LastLoc (Stop S)
then l in {(il. S,0 )} by Lm5;
then l = il. S,0 by TARSKI:def 1;
hence l = LastLoc (Stop S) by Th27; :: thesis: verum