0 .--> (goto l) = Load <*(goto l)*> by SCMFSA7B:3;
then reconsider I = 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 COMPOS_1:def 7;

now

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

end;

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