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