let I be preProgram of SCM+FSA; :: thesis: for a being Int-Location st not I destroys a holds
not Directed I destroys a
let a be Int-Location; :: thesis: ( not I destroys a implies not Directed I destroys a )
assume A1: not I destroys a ; :: thesis: not Directed I destroys a

now :: thesis: for i being Instruction of SCM+FSA st i in rng (Directed I) holds
not i destroys a

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

per cases ( I . x <> halt SCM+FSA or I . x = halt SCM+FSA ) ;

suppose I . x <> halt SCM+FSA ; :: thesis: not b₁ destroys a

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: verum

end;

suppose I . x = halt SCM+FSA ; :: thesis: not b₁ destroys a

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

end;

end;

end;

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