theorem :: SCMFSA8A:45

for I, J being NAT -defined the InstructionsF of SCM+FSA -valued Function st I c= J holds
for a being Int-Location st not J destroys a holds
not I destroys a