for P being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA
for I being good really-closed Program of SCM+FSA
for k being Nat holds (Comput ((P +* I),(Initialize s),k)) . (intloc 0) = s . (intloc 0) by SCMFSA7B:21, SCMFSA7B:def 5;