let I be Program of SCM+FSA ; :: thesis: for s being State of SCM+FSA st Initialized I c= s holds
s . (intloc 0 ) = 1
let s be State of SCM+FSA ; :: thesis: ( Initialized I c= s implies s . (intloc 0 ) = 1 )
A1: ( intloc 0 in dom (Initialized I) & (Initialized I) . (intloc 0 ) = 1 ) by SCMFSA6A:45, SCMFSA6A:46;
assume Initialized I c= s ; :: thesis: s . (intloc 0 ) = 1
hence s . (intloc 0 ) = 1 by A1, GRFUNC_1:8; :: thesis: verum