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