let I be Program of SCMPDS ; :: thesis: 0 in dom (stop I)
card (stop I) = (card I) + (card (Stop SCMPDS )) by Th45
.= (card I) + 1 by COMPOS_1:46 ;
hence 0 in dom (stop I) by AFINSQ_1:70; :: thesis: verum