let I be Program of SCMPDS ; :: thesis: ( inspos (card I) in dom (stop I) & (stop I) . (inspos (card I)) = halt SCMPDS )
set pI = stop I;
card (stop I) = (card I) + 1 by SCMPDS_5:7;
then card I < card (stop I) by XREAL_1:31;
hence inspos (card I) in dom (stop I) by SCMPDS_4:1; :: thesis: (stop I) . (inspos (card I)) = halt SCMPDS
set SS = Stop SCMPDS ;
A1: stop I = I ';' (Stop SCMPDS ) by SCMPDS_4:def 7;
(stop I) . (inspos (0 + (card I))) = halt SCMPDS by A1, SCMPDS_4:38, SCMPDS_4:73;
hence (stop I) . (inspos (card I)) = halt SCMPDS ; :: thesis: verum