theorem :: SCMFSA8C:14

for P being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA holds IExec ((Stop SCM+FSA),P,s) = Initialized s