0 .--> (goto l) = <%(goto l)%> by AFINSQ_1:def 1;
then reconsider I = 0 .--> (goto l) as Program of SCM+FSA ;
not halt SCM+FSA in rng I by Lm1;
hence Goto l is halt-free by COMPOS_1:def 3; :: thesis: Goto l is good
reconsider I = I as Program of SCM+FSA ;

now

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

end;

then not I destroys intloc 0 by SCMFSA7B:def 4;
hence Goto l is good by SCMFSA7B:def 5; :: thesis: verum