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