set F = Stop S;
LastLoc (Stop S) = 0 by Lm3;
hence (Stop S) . (LastLoc (Stop S)) = halt S ; :: according to COMPOS_1:def 14 :: thesis: verum