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

now

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

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

end;

suppose i in rng J ; :: thesis: b₁ does_not_destroy a

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

end;

end;

end;

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