let p be PartState of SCM+FSA; :: thesis: ( (Initialized p) . (intloc 0) = 1 & (Initialized p) . (IC ) = 0 )
intloc 0 in {(intloc 0)} by TARSKI:def 1;
then A1: intloc 0 in dom ((intloc 0) .--> 1) ;
A2: Initialized p = Initialize (p +* ((intloc 0) .--> 1)) by FUNCT_4:14;
intloc 0 <> IC by SCMFSA_2:56;
then not intloc 0 in {(IC )} by TARSKI:def 1;
then not intloc 0 in dom (Start-At (0,SCM+FSA)) ;
hence (Initialized p) . (intloc 0) = (p +* ((intloc 0) .--> 1)) . (intloc 0) by A2, FUNCT_4:11
.= ((intloc 0) .--> 1) . (intloc 0) by A1, FUNCT_4:13
.= 1 by FUNCOP_1:72 ;
:: thesis: (Initialized p) . (IC ) = 0
IC in {(IC )} by TARSKI:def 1;
then IC in dom (Start-At (0,SCM+FSA)) ;
hence (Initialized p) . (IC ) = (Start-At (0,SCM+FSA)) . (IC ) by A2, FUNCT_4:13
.= 0 by FUNCOP_1:72 ;
:: thesis: verum