let S be COM-Struct ; :: thesis: for I being Program of S holds 0 in dom (stop I)
let I be Program of S; :: thesis: 0 in dom (stop I)
card (stop I) = (card I) + (card (Stop S)) by AFINSQ_1:17
.= (card I) + 1 by AFINSQ_1:33 ;
hence 0 in dom (stop I) by AFINSQ_1:66; :: thesis: verum