theorem Th21: :: SCM_HALT:23

for s being State of SCM+FSA
for a being Int-Location
for p being Instruction-Sequence of SCM+FSA
for I being really-closed InitHalting keepInt0_1 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