thus (stop I) . (LastLoc (stop I)) = (stop I) . (card I) by Th57
.= halt S by Th48 ; :: according to COMPOS_1:def 14 :: thesis: verum