let a be Int-Location; :: thesis: for l being Nat holds not Goto l destroys a
let l be Nat; :: thesis: not Goto l destroys a

now :: thesis: for i being Instruction of SCM+FSA st i in rng (Goto l) holds
not i destroys a

let i be Instruction of SCM+FSA; :: thesis: ( i in rng (Goto l) implies not i destroys a )
A1: rng (Goto l) = {(goto l)} by AFINSQ_1:33;
assume i in rng (Goto l) ; :: thesis: not i destroys a
then i = goto l by A1, TARSKI:def 1;
hence not i destroys a ; :: thesis: verum

end;

hence not Goto l destroys a ; :: thesis: verum