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)
thus 0 in dom (stop I) by AFINSQ_1:66; :: thesis: verum