let S be COM-Struct ; :: thesis: for I being Program of S holds LastLoc (stop I) = card I
let I be Program of S; :: thesis: LastLoc (stop I) = card I
thus LastLoc (stop I) = (card (stop I)) -' 1 by AFINSQ_1:70
.= card I by Th55 ; :: thesis: verum