let i be Instruction of SCM+FSA; :: thesis: for a being Int-Location st not i refers a holds
not Macro i refers a
let a be Int-Location ; :: thesis: ( not i refers a implies not Macro i refers a )
A1: rng (Macro i) = {i,(halt SCM+FSA)} by FUNCT_4:67;
assume A2: not i refers a ; :: thesis: not Macro i refers a

now

let ii be Instruction of SCM+FSA; :: thesis: ( ii in rng (Macro i) implies not ii refers a )
assume ii in rng (Macro i) ; :: thesis: not ii refers a
then ( ii = i or ii = halt SCM+FSA ) by A1, TARSKI:def 2;
hence not ii refers a by A2, Th78; :: thesis: verum

end;

hence not Macro i refers a by SCMFSA7B:def 2; :: thesis: verum