let i be Instruction of SCM+FSA; :: thesis: for a being Int-Location st not i destroys a holds
not Macro i destroys a
let a be Int-Location; :: thesis: ( not i destroys a implies not Macro i destroys a )
A1: rng (Macro i) = {i,(halt SCM+FSA)} by COMPOS_1:67;
assume not i destroys a ; :: thesis: not Macro i destroys a
then for ii being Instruction of SCM+FSA st ii in rng (Macro i) holds
not ii destroys a by A1, TARSKI:def 2;
hence not Macro i destroys a ; :: thesis: verum