theorem Th7: :: SCM_HALT:9

for s being State of SCM+FSA
for p being Instruction-Sequence of SCM+FSA
for I being InitHalting keepInt0_1 Program of SCM+FSA holds (IExec (I,p,s)) . (intloc 0) = 1