let S be COM-Struct ; :: thesis: LastLoc (Stop S) = 0
(card (Stop S)) -' 1 = 0 by Lm2;
hence LastLoc (Stop S) = 0 by AFINSQ_1:70; :: thesis: verum