rng (Macro i) = {i,(halt SCM+FSA)} by FUNCT_4:67;
then i in rng (Macro i) by TARSKI:def 2;
then C: ( not Macro i destroys intloc 0 implies not i destroys intloc 0 ) by SCMFSA7B:def 4;
A: ( not i destroys intloc 0 implies not Macro i destroys intloc 0 ) by SCMFSA8C:77;
( Macro i is good iff i is good ) by SFMASTR1:def 1;
hence ( i is good iff not i destroys intloc 0 ) by A, C, SCMFSA7B:def 5; :: thesis: verum