theorem Th7: :: SCMFSA6C:8

for a being Int-Location
for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA
for i being sequential keeping_0 Instruction of SCM+FSA
for j being sequential Instruction of SCM+FSA holds (IExec ((i ";" j),P,s)) . a = (Exec (j,(Exec (i,(Initialized s))))) . a