(insloc 0 ) .--> (goto l) = Load <*(goto l)*> by SCMFSA7B:3;
then reconsider I = (insloc 0 ) .--> (goto l) as Program of SCM+FSA ;
not halt SCM+FSA in rng I by Lm1;
then reconsider I = I as halt-free Program of SCM+FSA by AMI_1:def 52;

now

let x be Instruction of SCM+FSA ; :: thesis: ( x in rng ((insloc 0 ) .--> (goto l)) implies x does_not_destroy intloc 0 )
assume A1: x in rng ((insloc 0 ) .--> (goto l)) ; :: thesis: x does_not_destroy intloc 0
rng ((insloc 0 ) .--> (goto l)) = {(goto l)} by FUNCOP_1:14;
then x = goto l by A1, TARSKI:def 1;
hence x does_not_destroy intloc 0 by SCMFSA7B:17; :: thesis: verum

end;

then I does_not_destroy intloc 0 by SCMFSA7B:def 4;
hence (insloc 0 ) .--> (goto l) is halt-free good Program of SCM+FSA by SCMFSA7B:def 5; :: thesis: verum