theorem Th13: :: SFMASTR1:14

for p being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA
for i being sequential good Instruction of SCM+FSA
for a being Int-Location
for J being really-closed Program of SCM+FSA st ( J is parahalting or J is_halting_on Exec (i,(Initialized s)),p ) holds
(IExec ((i ";" J),p,s)) . a = (IExec (J,p,(Exec (i,(Initialized s))))) . a