0 .--> (goto l) = <%(goto l)%> by AFINSQ_1:def 2;
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 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 destroys intloc 0 )
A1: rng (0 .--> (goto l)) = {(goto l)} by FUNCOP_1:14;
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:17; :: thesis: verum

end;

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