theorem Th1: :: SCMFSA9A:1

for l being Nat
for i being Instruction of SCM+FSA holds UsedILoc (l .--> i) = UsedIntLoc i