let p be Instruction-Sequence of SCM+FSA; for s being State of SCM+FSA
for i being sequential good Instruction of SCM+FSA
for J being really-closed Program of SCM+FSA st ( J is parahalting or J is_halting_on Exec (i,(Initialized s)),p ) holds
DataPart (IExec ((i ";" J),p,s)) = DataPart (IExec (J,p,(Exec (i,(Initialized s)))))
let s be State of SCM+FSA; for i being sequential good Instruction of SCM+FSA
for J being really-closed Program of SCM+FSA st ( J is parahalting or J is_halting_on Exec (i,(Initialized s)),p ) holds
DataPart (IExec ((i ";" J),p,s)) = DataPart (IExec (J,p,(Exec (i,(Initialized s)))))
let i be sequential good Instruction of SCM+FSA; for J being really-closed Program of SCM+FSA st ( J is parahalting or J is_halting_on Exec (i,(Initialized s)),p ) holds
DataPart (IExec ((i ";" J),p,s)) = DataPart (IExec (J,p,(Exec (i,(Initialized s)))))
let J be really-closed Program of SCM+FSA; ( ( J is parahalting or J is_halting_on Exec (i,(Initialized s)),p ) implies DataPart (IExec ((i ";" J),p,s)) = DataPart (IExec (J,p,(Exec (i,(Initialized s))))) )
assume A1:
( J is parahalting or J is_halting_on Exec (i,(Initialized s)),p )
; DataPart (IExec ((i ";" J),p,s)) = DataPart (IExec (J,p,(Exec (i,(Initialized s)))))
then A2:
for f being FinSeq-Location holds (IExec ((i ";" J),p,s)) . f = (IExec (J,p,(Exec (i,(Initialized s))))) . f
by Th14;
for a being Int-Location holds (IExec ((i ";" J),p,s)) . a = (IExec (J,p,(Exec (i,(Initialized s))))) . a
by A1, Th13;
hence
DataPart (IExec ((i ";" J),p,s)) = DataPart (IExec (J,p,(Exec (i,(Initialized s)))))
by A2, SCMFSA_M:2; verum