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