let I be Program of SCMPDS ; :: thesis: (Initialized I) . (IC SCMPDS ) = 0
IC SCMPDS in {(IC SCMPDS )} by TARSKI:def 1;
then IC SCMPDS in dom (Start-At 0 ,SCMPDS ) by FUNCOP_1:19;
hence (Initialized I) . (IC SCMPDS ) = (Start-At 0 ,SCMPDS ) . (IC SCMPDS ) by FUNCT_4:14
.= 0 by FUNCOP_1:87 ;
:: thesis: verum