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