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 )
assume A1: Initialized I c= s ; :: thesis: s . (intloc 0 ) = 1
A2: intloc 0 in dom (Initialized I) by SCMFSA6A:45;
(Initialized I) . (intloc 0 ) = 1 by SCMFSA6A:46;
hence s . (intloc 0 ) = 1 by A1, A2, GRFUNC_1:8; :: thesis: verum