let I, J be NAT -defined the InstructionsF of SCM+FSA -valued Function; :: thesis: ( I c= J implies for a being Int-Location st not J destroys a holds
not I destroys a )
assume A1: I c= J ; :: thesis: for a being Int-Location st not J destroys a holds
not I destroys a
let a be Int-Location; :: thesis: ( not J destroys a implies not I destroys a )
assume A2: not J destroys a ; :: thesis: not I destroys a
let i be Instruction of SCM+FSA; :: according to SCMFSA7B:def 4 :: thesis: ( not i in rng I or not i destroys a )
assume A3: i in rng I ; :: thesis: not i destroys a
rng I c= rng J by A1, RELAT_1:11;
then i in rng J by A3;
hence not i destroys a by A2, SCMFSA7B:def 4; :: thesis: verum