let a be Int-Location ; :: thesis: for l being Instruction-Location of SCM+FSA holds Goto l does_not_destroy a
let l be Instruction-Location of SCM+FSA ; :: thesis: Goto l does_not_destroy a

now

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

end;

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