let l1, l2 be Instruction-Location of SCM+FSA ; :: thesis: for a being Int-Location holds l1 .--> (goto l2) does_not_destroy a
let a be Int-Location ; :: thesis: l1 .--> (goto l2) does_not_destroy a
set I = l1 .--> (goto l2);
A1: rng (l1 .--> (goto l2)) = {(goto l2)} by FUNCOP_1:14;

now

let i be Instruction of SCM+FSA ; :: thesis: ( i in rng (l1 .--> (goto l2)) implies i does_not_destroy a )
assume i in rng (l1 .--> (goto l2)) ; :: thesis: i does_not_destroy a
then i = goto l2 by A1, TARSKI:def 1;
hence i does_not_destroy a by SCMFSA7B:17; :: thesis: verum

end;

hence l1 .--> (goto l2) does_not_destroy a by SCMFSA7B:def 4; :: thesis: verum