let I, J be preProgram of SCM+FSA; :: thesis: for a being Int-Location st not I destroys a & not J destroys a holds
not I +* J destroys a
let a be Int-Location; :: thesis: ( not I destroys a & not J destroys a implies not I +* J destroys a )
assume A1: not I destroys a ; :: thesis: ( J destroys a or not I +* J destroys a )
assume A2: not J destroys a ; :: thesis: not I +* J destroys a

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

let i be Instruction of SCM+FSA; :: thesis: ( i in rng (I +* J) implies not b₁ destroys a )
A3: rng (I +* J) c= (rng I) \/ (rng J) by FUNCT_4:17;
assume A4: i in rng (I +* J) ; :: thesis: not b₁ destroys a

per cases ( i in rng I or i in rng J ) by A4, A3, XBOOLE_0:def 3;

suppose i in rng I ; :: thesis: not b₁ destroys a

hence not i destroys a by A1, SCMFSA7B:def 4; :: thesis: verum

end;

suppose i in rng J ; :: thesis: not b₁ destroys a

hence not i destroys a by A2, SCMFSA7B:def 4; :: thesis: verum

end;

end;

end;

hence not I +* J destroys a by SCMFSA7B:def 4; :: thesis: verum