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

now

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

end;

hence Macro i does_not_destroy a by SCMFSA7B:def 4; :: thesis: verum