let a be Int-Location ; :: thesis: for l being Element of NAT holds not Goto l destroysdestroy a
let l be Element of NAT ; :: thesis: not Goto l destroysdestroy a

now

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

end;

hence not Goto l destroysdestroy a by SCMFSA7B:def 4; :: thesis: verum