now

let i be Instruction of SCM+FSA ; :: thesis: ( i in rng (Stop SCM+FSA ) implies i does_not_destroy intloc 0 )
assume A1: i in rng (Stop SCM+FSA ) ; :: thesis: i does_not_destroy intloc 0
rng (Stop SCM+FSA ) = {(halt SCM+FSA )} by AFINSQ_1:36;
then i = halt SCM+FSA by A1, TARSKI:def 1;
hence i does_not_destroy intloc 0 by Th11; :: thesis: verum

end;

hence Stop SCM+FSA does_not_destroy intloc 0 by Def4; :: thesis: verum