let I be Program of SCM+FSA; :: thesis: for s being State of SCM+FSA st Initialize ((intloc 0) .--> 1) c= s holds
s . (intloc 0) = 1
let s be State of SCM+FSA; :: thesis: ( Initialize ((intloc 0) .--> 1) c= s implies s . (intloc 0) = 1 )
Y: 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 A1: intloc 0 in dom (Initialize ((intloc 0) .--> 1)) by Y, XBOOLE_0:def 3;
C: dom (Start-At (0,SCM+FSA)) = {(IC )} by FUNCOP_1:13;
IC <> intloc 0 by SCMFSA_2:56;
then not intloc 0 in dom (Start-At (0,SCM+FSA)) by C, TARSKI:def 1;
then B1: (Initialize ((intloc 0) .--> 1)) . (intloc 0) = ((intloc 0) .--> 1) . (intloc 0) by FUNCT_4:11
.= 1 by FUNCOP_1:72 ;
assume Initialize ((intloc 0) .--> 1) c= s ; :: thesis: s . (intloc 0) = 1
hence s . (intloc 0) = 1 by A1, B1, GRFUNC_1:2; :: thesis: verum