let l1, l2 be Element of NAT ; :: thesis: for a being Int-Location holds not l1 .--> (goto l2) destroys a
let a be Int-Location ; :: thesis: not l1 .--> (goto l2) destroys a
set I = l1 .--> (goto l2);
A1: rng (l1 .--> (goto l2)) = {(goto l2)} by FUNCOP_1:8;

now

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

end;

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