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 b1 destroys a )
A3: rng (I +* J) c= (rng I) \/ (rng J) by FUNCT_4:17;
assume A4: i in rng (I +* J) ; :: thesis: not b1 destroys a
per cases ( i in rng I or i in rng J ) by A4, A3, XBOOLE_0:def 3;
end;
end;
hence not I +* J destroys a by SCMFSA7B:def 4; :: thesis: verum