let I be Program of SCM+FSA; :: thesis: ( (Initialized I) . (intloc 0) = 1 & (Initialized I) . (IC ) = 0 )
intloc 0 in {(intloc 0)} by TARSKI:def 1;
then A1: intloc 0 in dom ((intloc 0) .--> 1) by FUNCOP_1:19;
A2: Initialized I = Initialize (I +* ((intloc 0) .--> 1)) by FUNCT_4:15;
intloc 0 <> IC by SCMFSA_2:81;
then not intloc 0 in {(IC )} by TARSKI:def 1;
then not intloc 0 in dom (Start-At (0,SCM+FSA)) by FUNCOP_1:19;
hence (Initialized I) . (intloc 0) = (I +* ((intloc 0) .--> 1)) . (intloc 0) by FUNCT_4:12, A2
.= ((intloc 0) .--> 1) . (intloc 0) by A1, FUNCT_4:14
.= 1 by FUNCOP_1:87 ;
:: thesis: (Initialized I) . (IC ) = 0
IC in {(IC )} by TARSKI:def 1;
then IC in dom (Start-At (0,SCM+FSA)) by FUNCOP_1:19;
hence (Initialized I) . (IC ) = (Start-At (0,SCM+FSA)) . (IC ) by FUNCT_4:14, A2
.= 0 by FUNCOP_1:87 ;
:: thesis: verum