let I be preProgram of SCM+FSA; :: thesis:
let a be Int-Location; :: thesis:
assume A1: not I destroys a ; :: thesis:

let i be Instruction of SCM+FSA; :: thesis:
A2: dom (Directed I) = dom I by FUNCT_4:99;
assume i in rng (Directed I) ; :: thesis:
then consider x being object such that
A3: x in dom (Directed I) and
A4: i = (Directed I) . x by FUNCT_1:def 3;

suppose I . x <> halt SCM+FSA ; :: thesis:

then i = I . x by A4, FUNCT_4:105;
then i in rng I by A3, A2, FUNCT_1:def 3;
hence not i destroys a by A1, SCMFSA7B:def 4; :: thesis:

end;

suppose I . x = halt SCM+FSA ; :: thesis:

then i = goto (card I) by A3, A4, A2, FUNCT_4:106;
hence not i destroys a by SCMFSA7B:11; :: thesis:

end;

end;

end;

hence not Directed I destroys a by SCMFSA7B:def 4; :: thesis: