rng (Macro i) = {i,(halt SCM+FSA)}
by COMPOS_1:67;

then i in rng (Macro i) by TARSKI:def 2;

then A1: ( not Macro i destroys intloc 0 implies not i destroys intloc 0 ) ;

A2: ( not i destroys intloc 0 implies not Macro i destroys intloc 0 ) by SCMFSA8C:48;

( Macro i is good iff i is good ) by SFMASTR1:def 1;

hence ( i is good iff not i destroys intloc 0 ) by A2, A1; :: thesis: verum

then i in rng (Macro i) by TARSKI:def 2;

then A1: ( not Macro i destroys intloc 0 implies not i destroys intloc 0 ) ;

A2: ( not i destroys intloc 0 implies not Macro i destroys intloc 0 ) by SCMFSA8C:48;

( Macro i is good iff i is good ) by SFMASTR1:def 1;

hence ( i is good iff not i destroys intloc 0 ) by A2, A1; :: thesis: verum