thus (Stop S) . (LastLoc (Stop S)) = (0 .--> (halt S)) . 0 by Lm3
.= halt S by FUNCOP_1:72 ; :: according to COMPOS_1:def 14 :: thesis: Stop S is unique-halt
let l be Nat; :: according to COMPOS_1:def 15 :: thesis: ( (Stop S) . l = halt S & l in dom (Stop S) implies 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 {0} ;
then l = 0 by TARSKI:def 1;
hence l = LastLoc (Stop S) by Lm3; :: thesis: verum