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 & UsedInt*Loc pc = UsedInt*Loc ic ) holds
UsedI*Loc p = UsedI*Loc (p +* (l,ic))