let s be State of SCM+FSA; :: thesis: ( Initialize ((intloc 0) .--> 1) c= s implies s . (intloc 0) = 1 )
set iS = Initialize ((intloc 0) .--> 1);
A1: dom (Initialize ((intloc 0) .--> 1)) = (dom ((intloc 0) .--> 1)) \/ (dom (Start-At (0,SCM+FSA))) by FUNCT_4:def 1;
intloc 0 in dom ((intloc 0) .--> 1) by FUNCOP_1:74;
then A2: intloc 0 in dom (Initialize ((intloc 0) .--> 1)) by A1, XBOOLE_0:def 3;
IC <> intloc 0 by SCMFSA_2:56;
then not intloc 0 in dom (Start-At (0,SCM+FSA)) by TARSKI:def 1;
then (Initialize ((intloc 0) .--> 1)) . (intloc 0) = ((intloc 0) .--> 1) . (intloc 0) by FUNCT_4:11
.= 1 by FUNCOP_1:72 ;
hence ( Initialize ((intloc 0) .--> 1) c= s implies s . (intloc 0) = 1 ) by A2, GRFUNC_1:2; :: thesis: verum