theorem :: SCMFSA_9:49

for p being preProgram of SCM+FSA
for l being Nat
for ic being Instruction of SCM+FSA st ex pc being Instruction of SCM+FSA st
( pc = p . l & UsedIntLoc pc = UsedIntLoc ic ) holds
UsedILoc p = UsedILoc (p +* (l,ic))