theorem Th57: :: SCMFSA8C:66

for P being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA
for I being good Program of SCM+FSA
for m being Nat st ( for n being Nat st n < m holds
IC (Comput ((P +* I),(Initialize s),n)) in dom I ) holds
for n being Nat st n <= m holds
(Comput ((P +* I),(Initialize s),n)) . (intloc 0) = s . (intloc 0) by Th56, SCMFSA7B:def 5;