theorem Th5: :: SCMFSA6C:6

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