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

now

let i be Instruction of SCM+FSA ; :: thesis: ( i in rng (I +* J) implies not b₁ destroysdestroy a )
A3: rng (I +* J) c= (rng I) \/ (rng J) by FUNCT_4:18;
assume A4: i in rng (I +* J) ; :: thesis: not b₁ destroysdestroy 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₁ destroysdestroy a

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

end;

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

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

end;

end;

end;

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