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 SCMNORM:3 ;
hence 0 in dom (stop I) by Th1; :: thesis: verum