theorem :: SFMASTR2:8

for b being Int-Location
for I being MacroInstruction of SCM+FSA holds {b} \/ (UsedILoc I) c= UsedILoc (times (b,I))