let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite realistic COM-Struct of N
for I being Program of S holds 0 in dom (stop I)
let S be non empty stored-program IC-Ins-separated definite realistic COM-Struct of N; :: 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:20
.= (card I) + 1 by Th46 ;
hence 0 in dom (stop I) by AFINSQ_1:70; :: thesis: verum