let I be Program of SCM+FSA; :: thesis: for a being Int-Location
for k being Nat
for i being Instruction of SCM+FSA st not I destroys a & not i destroys a holds
not I +* (k,i) destroys a
let a be Int-Location; :: thesis: for k being Nat
for i being Instruction of SCM+FSA st not I destroys a & not i destroys a holds
not I +* (k,i) destroys a
let k be Nat; :: thesis: for i being Instruction of SCM+FSA st not I destroys a & not i destroys a holds
not I +* (k,i) destroys a
let i be Instruction of SCM+FSA; :: thesis: ( not I destroys a & not i destroys a implies not I +* (k,i) destroys a )
assume that
A1: not I destroys a and
A2: not i destroys a ; :: thesis: not I +* (k,i) destroys a
let j be Instruction of SCM+FSA; :: according to SCMFSA7B:def 4 :: thesis: ( not j in rng (I +* (k,i)) or not j destroys a )
assume A3: j in rng (I +* (k,i)) ; :: thesis: not j destroys a
rng (I +* (k,i)) c= (rng I) \/ {i} by FUNCT_7:100;
then j in (rng I) \/ {i} by A3;

per cases then ( j in rng I or j in {i} ) by XBOOLE_0:def 3;

suppose j in rng I ; :: thesis: not j destroys a

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

end;

suppose j in {i} ; :: thesis: not j destroys a

hence not j destroys a by A2, TARSKI:def 1; :: thesis: verum

end;

end;